Theorem: QuadRing.min_eq_top_iff (ECTate/Algebra/QuadRing/Valuations.lean)

State before:
a b : ℕ∞
⊢ min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤
Tactic:
sorry
State after:
no goals