Working with inequalities

Stream: lean4

[Omnikar]

How do I, for example, construct a proof that a / 2 > 4 given that a > 8?

example (a : Nat) (h : a > 8) : a / 2 > 4 := sorry

[Mario Carneiro]

It's false...

[Mario Carneiro]

example : ¬∀ (a : Nat) (h : a > 8), a / 2 > 4 :=
  mt (· 9) (by decide)

(pointlessly golfed)

[Omnikar]

Oh I forgot about that. In that case, what if you change the 8 to say 10? Then a/2 should be greater than 4.

[Mario Carneiro]

import Std.Data.Nat.Lemmas

example (a : Nat) (h : a > 9) : a / 2 > 4 :=
  (Nat.le_div_iff_mul_le (by decide)).2 h

[Omnikar]

Other question: I've found that you can prove n < 2 given n < 1 like this, but is there a shorter way to express this?

example (n : Nat) (h : n < 1) : n < 2 := Trans.trans h (show 1 < 2 by simp)

[Mario Carneiro]

that last line is (by decide) as well

[Omnikar]

How do I show False given n : Nat and h : n < 0?

[Henrik Böving]

I would

example {n : Nat} (h : n < 0) : False := by
  cases n <;> cases h

[Omnikar]

Thanks

[Omnikar]

Oh, I just found out about Nat.not_lt_zero which I think is a way more readable way to do it.