Theorem: ENat.toNat_le_of_leNat (GMLInit/Data/Nat/Extended/Finite.lean)

State before:
e : ENat
x : Nat
h : e.leNat x = true
⊢ e.toNat ⋯ ≤ x
Tactic:
apply toNatAux_le h
State after:
e : ENat
x : Nat
h : e.leNat x = true
⊢ 0 ≤ x

State before:
e : ENat
x : Nat
h : e.leNat x = true
⊢ 0 ≤ x
Tactic:
exact Nat.zero_le x
State after:
no goals