norm_num and fact

Stream: maths

[Kevin Buzzard]

import data.nat.basic
import tactic.norm_num

open nat

example : fact 7 ≥ 3 ^ 7 :=
begin
--  unfold fact, norm_num, -- fails, perhaps because of succ's
  show 7 * (6 * (5 * (4 * (3 * (2 * (1 * 1)))))) ≥ 3 ^ 7,
  norm_num,
end

@Mario Carneiro Can you get norm_num to know enough about fact to make this work? After unfolding fact I get a goal with a lot of nat.succ's in. Or is this harder than it looks?

[Mario Carneiro]

I think you can rewrite nat.succ to +1 and then apply norm_num

[Mario Carneiro]

example : fact 7 ≥ 3 ^ 7 :=
by dsimp only [fact, succ_eq_add_one]; norm_num