Shortest proof challenge

Stream: general

[Chris Hughes]

example (a b : ℕ) : a ≠ b → 0 < a + b

[Kevin Buzzard]

nat.rec (nat.pos_of_ne_zero) (λ n H I, nat.zero_lt_succ _) b (or smaller if I'm allowed to open nat)

[Kevin Buzzard]

These games are slightly artificial because a lot depends on whether the things you want are already in lean.

[Kevin Buzzard]

nat.rec (nat.pos_of_ne_zero) (λ_ H I, nat.zero_lt_succ _) b cheating a character away

[Chris Hughes]

Thanks. I need this one as well

lemma  nat.div_mul_le (a : ℕ) {b : ℕ} (hb : 0  < b) : a / b * b ≤ a

[Kevin Buzzard]

I think induction on b might fare less well this time.

[Kenny Lau]

nat.rec (nat.pos_of_ne_zero) (λ_ H I, nat.zero_lt_succ _) b cheating a character away

you don't need parentheses to enclose something without space