Theorem: ENat.lt_one_iff (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
n : ℕ∞
⊢ n < 1 ↔ n = 0
Tactic:
rw [← not_iff_not, not_lt, ENat.one_le_iff_ne_zero]
State after:
no goals