cases h n with
| inl h => rw [leNat_coe_eq_true_iff_le] at h; absurd h; exact Nat.lt_irrefl n
| inr h => exists n; rw [leNat_coe_eq_true_iff_le]; exact ⟨Nat.le_refl n, h⟩
case mpr
n : Nat
x : ENat
h : ENat.ofNat (n + 1) ≤ x
⊢ ENat.ofNat n < x
no goals