apply mt _ hx
case leNat.h.false
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ ¬(ENat.ofNat (e.toNat h)).leNat x = true
e : ENat
h : e.IsFinite
x : Nat
hx : ¬e.leNat x = true
⊢ (ENat.ofNat (e.toNat h)).leNat x = true → e.leNat x = true