nat case bashing

Stream: maths

[Sebastien Gouezel]

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).

[Chris Hughes]

omega?

[Sebastien Gouezel]

Yes, thanks!