Zulip Chat Archive

Stream: general

Topic: Shortest proof challenge


view this post on Zulip Chris Hughes (Apr 05 2018 at 19:57):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:23):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:23):

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 20:24):

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

view this post on Zulip Chris Hughes (Apr 05 2018 at 20:54):

Thanks. I need this one as well

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

view this post on Zulip Kevin Buzzard (Apr 05 2018 at 21:13):

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

view this post on Zulip Kenny Lau (Apr 05 2018 at 23:11):

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


Last updated: May 12 2021 at 23:13 UTC