rw [toNatAux_eq]
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
⊢ ENat.toNatAux ⋯ x ≤ y
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
⊢ (if e.leNat x = true then x else ENat.toNatAux ⋯ (x + 1)) ≤ y