rw [leNat_coe_eq_true_iff_le] at h
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : (ENat.ofNat (n + 1)).leNat n = true
⊢ ENat.ofNat n < x
case mpr.inl
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : n + 1 ≤ n
⊢ ENat.ofNat n < x