cases Nat.lt_or_ge n k with
| inl hlt => left; exact hlt
| inr hge => right; apply mono' hge; apply mono' h; exact hm
case mp
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
k : Nat
⊢ n + 1 ≤ k ∨ x.leNat k = false
no goals