Proving succ a ≤ zero is obviously false

Stream: new members

[Brandon Brown]

I've been making good progress learning how to prove a bunch of basic things about the less-than-or-equal-to relation on the natural numbers, but I realize I do not really understand how to prove something is false. Any hints on this one? It's obviously false because that's how I've defined my nat.le function but I don't know how to put that on the right side of my theorem. This is Lean4 code.

inductive nat : Type where
| zero : nat
| succ : nat → nat

open nat

protected def nat.ple (a b : nat) : Bool :=
  match a, b with
  | zero, b => true
  | succ a, zero => false
  | succ a, succ b => nat.ple a b

protected def nat.le (a b : nat) : Prop := nat.ple a b = true

theorem succ_le_zero_false {a : nat} : (nat.le a.succ zero) → false := sorry

[Johan Commelin]

Can you show nat.ple a.succ zero = false?

[Eric Wieser]

Lean 4 doesn't have equation lemmas (yet), right?

[Daniel Fabian]

theorem succ_le_zero_false {a : nat} : (nat.le a.succ zero) → false := fun h => by
  cases h

[Daniel Fabian]

you can use dependent elimination.

[Daniel Fabian]

by a distinction by cases on something that's false, i.e. it has 0 constructors, the goal closes automatically.