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

State before:
m n : Nat
⊢ (ENat.ofNat n).leNat m = true ↔ n ≤ m
Tactic:
rw [ENat.ofNat, Nat.ble_eq]
State after:
no goals