rw [leNat_coe_eq_true_iff_le] at h
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
⊢ x.leNat n = false
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
⊢ x.leNat n = false