norm_num produces bad proof term

Stream: general

[Bhavik Mehta]

Here's my example:

import tactic.norm_num

lemma covering_one_aux : ∀ n, n = 6 → ¬n % 4 = 0 → false :=
begin
  rintro (_ | _ | _ | _ | _ | _ | _ | _) h,
  work_on_goal 7 {norm_num1},
  all_goals {sorry},
end

and it produces the error

type mismatch at application
  norm_num.one_add 2 5 (norm_num.bit0_succ 1)
term
  norm_num.bit0_succ 1
has type
  2 + 1 = 3
but is expected to have type
  2 + 1 = 5

[Mario Carneiro]

#17415

[Bhavik Mehta]

Thanks!