intro hx
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ (ENat.ofNat (e.toNat h)).leNat x = true → e.leNat x = true
e : ENat
h : e.IsFinite
x : Nat
hx✝ : ¬e.leNat x = true
hx : (ENat.ofNat (e.toNat h)).leNat x = true
⊢ e.leNat x = true