intro h
case succ
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
⊢ x ≤ ENat.ofNat (n + 1) → ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
case succ
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m