norm_num and nat.fact

Stream: general

[Reid Barton]

norm_num doesn't seem to know what to do with nat.succ:

example : nat.fact 5 = 120 := begin
  norm_num,
  -- ⊢ nat.succ 4 * (nat.succ 3 * (nat.succ 2 * nat.succ 1)) = 120
end

[Reid Barton]

But when I try a simpler example like nat.succ 5 = 6, it does work for some reason

[Kevin Buzzard]

You clearly need to use more powerful automation like rfl

[Floris van Doorn]

Ah, I'm not the only one doing IMO 2019-4 :)

[Floris van Doorn]

I used norm_num [finset.range_succ, nat.pow_succ, nat.mul_succ] for the easy direction.

[Floris van Doorn]

I'm stuck on prime (2 : ℤ) (the definition of prime for rings :) )

[Johan Commelin]

Didn't Chris prove that primes in nat are primes in int?

[Floris van Doorn]

Is it in mathlib? I cannot find it.