Zulip Chat Archive

Stream: maths

Topic: nat case bashing


view this post on Zulip Sebastien Gouezel (Feb 25 2020 at 17:31):

Is there a good proof of

lemma zou (n : ) (hn : n  1) (h: n  0) : n = 1 :=
by simpa [nat.lt_succ_iff, nat.le_zero_iff, h] using lt_or_eq_of_le hn

(I mean, other than waiting for #1596 -- I would love this to get into mathlib, but I don't feel qualified to review it).

view this post on Zulip Chris Hughes (Feb 25 2020 at 17:43):

omega?

view this post on Zulip Sebastien Gouezel (Feb 25 2020 at 17:54):

Yes, thanks!


Last updated: May 06 2021 at 18:20 UTC