rw [leNat_eq_true_iff_le_coe] at hn
case succ.true
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : x.leNat n = true
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m
case succ.true
x : ENat
n : Nat
ih : x ≤ ENat.ofNat n → ∃ m, m ≤ n ∧ x = ENat.ofNat m
h : x ≤ ENat.ofNat (n + 1)
hn : x ≤ ENat.ofNat n
⊢ ∃ m, m ≤ n + 1 ∧ x = ENat.ofNat m