rw [leNat_coe_eq_false_iff_gt]
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ (ENat.ofNat n).leNat k = false
case inl.h
x : ENat
n : Nat
h : x.leNat n = true
k : Nat
hlt : k < n
⊢ k < n