should this be dec_trivial?

Stream: maths

[Kevin Buzzard]

example (n : ℕ) : n > 0 → n ≤ 6 → fact n < 3 ^ n := dec_trivial -- fails

I do 6 case splits and dec_trivial seems to be able to handle the arithmetic, but I can't do it all in one go. I sometimes run into these. How is one supposed to diagnose what has happened and fix it?

[Chris Hughes]

Revert n, and put n \le 6 before 0<n

[Kevin Buzzard]

Thanks Chris.

[Kevin Buzzard]

I see, so forall n : nat, n <= X -> P n works, and I just need to ensure I'm in this format.

[Mario Carneiro]

sigh... why the horrible case split proofs?

[Mario Carneiro]

you could reason it instead

[Kevin Buzzard]

I don't really know what you're saying

[Kevin Buzzard]

or even if you're talking to me

[Kevin Buzzard]

But my job is to solve the problems I set, in Lean

[Mario Carneiro]

if you had to prove that theorem by hand I am sure you wouldn't evaluate 6 factorials

[Kevin Buzzard]

and the problem is "for which positive integers n is n! < 3^n"

[Mario Carneiro]

you can prove that it's true for 5 and stop because monotonicity

[Kevin Buzzard]

ha ha

[Kevin Buzzard]

I'm not sure it's that easy

[Kevin Buzzard]

n! and 3^n are changing in different ways

[Kevin Buzzard]

and things get weird at n=3

[Kevin Buzzard]

I think I have to check all 6

[Kevin Buzzard]

dec_trivial times out for 7 :-/

[Kevin Buzzard]

(hence the norm_num approach, which was also troublesome -- see other thread)