match hx : x.leNat n, hy : y.leNat n with
| false, _ => right; rfl
| _, true => left; rfl
| true, false => absurd h; exists n
case mp
x y : ENat
h : ¬x < y
n : Nat
⊢ y.leNat n = true ∨ x.leNat n = false
no goals