cases Nat.lt_or_ge k n with
| inl hlt => right; rw [leNat_coe_eq_false_iff_gt]; exact hlt
| inr hge => left; exact mono hge h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
⊢ x.leNat k = true ∨ (ENat.ofNat n).leNat k = false
no goals