rw [toNatAux_eq]
e : ENat
isFinite : e.IsFinite
x : Nat
⊢ e.leNat (ENat.toNatAux isFinite x) = true
e : ENat
isFinite : e.IsFinite
x : Nat
⊢ e.leNat (if e.leNat x = true then x else ENat.toNatAux isFinite (x + 1)) = true