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

State before:
m n : Nat
⊢ (ENat.ofNat n).leNat m = false ↔ m < n
Tactic:
rw [Bool.eq_false_iff, ←Nat.not_le, ←leNat_coe_eq_true_iff_le]
State after:
no goals