Theorem: ENat.leNat_zero_eq_true (GMLInit/Data/Nat/Extended/Basic.lean)

State before:
n : Nat
⊢ leNat 0 n = true
Tactic:
simp only [OfNat.ofNat, leNat_coe_eq_true_iff_le, Nat.zero_le]
State after:
no goals