Zulip Chat Archive
Stream: general
Topic: eliminating impossible cases
Reid Barton (Dec 20 2018 at 19:16):
If I have hi : i < 0 as a hypothesis (i is a nat), what tactic will let me solve the goal most efficiently?
Reid Barton (Dec 20 2018 at 19:17):
Is exact absurd hi (nat.not_lt_zero _) really the easiest way?
Kenny Lau (Dec 20 2018 at 19:17):
cases hi
Last updated: May 02 2025 at 03:31 UTC