intro ⟨m, h, hm⟩ k
case mp
n : Nat
x : ENat
⊢ ENat.ofNat n < x → ENat.ofNat (n + 1) ≤ x
case mp
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
k : Nat
⊢ (ENat.ofNat (n + 1)).leNat k = true ∨ x.leNat k = false