## Stream: maths

### Topic: should this be dec_trivial?

#### Kevin Buzzard (Nov 18 2018 at 15:26):

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 (Nov 18 2018 at 15:27):

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

Thanks Chris.

#### Kevin Buzzard (Nov 18 2018 at 15:28):

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

#### Mario Carneiro (Nov 18 2018 at 15:58):

sigh... why the horrible case split proofs?

#### Kevin Buzzard (Nov 18 2018 at 15:58):

I don't really know what you're saying

#### Kevin Buzzard (Nov 18 2018 at 15:59):

or even if you're talking to me

#### Kevin Buzzard (Nov 18 2018 at 15:59):

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

#### Mario Carneiro (Nov 18 2018 at 15:59):

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

#### Kevin Buzzard (Nov 18 2018 at 15:59):

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

#### Mario Carneiro (Nov 18 2018 at 16:00):

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

ha ha

#### Kevin Buzzard (Nov 18 2018 at 16:00):

I'm not sure it's that easy

#### Kevin Buzzard (Nov 18 2018 at 16:00):

n! and 3^n are changing in different ways

#### Kevin Buzzard (Nov 18 2018 at 16:00):

and things get weird at n=3

#### Kevin Buzzard (Nov 18 2018 at 16:00):

I think I have to check all 6

#### Kevin Buzzard (Nov 18 2018 at 16:01):

dec_trivial times out for 7 :-/

#### Kevin Buzzard (Nov 18 2018 at 16:01):

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

Last updated: May 12 2021 at 07:17 UTC