m n k l : ℕ
⊢ m + n = min m n ↔ max m n = 0
m n k l : ℕ
⊢ m + n = min m n ↔ m = 0 ∧ n = 0
rw [← max_eq_zero_iff]
no goals
m n k l : ℕ
⊢ m + n = min m n ↔ max m n = 0
cases' le_total m n with H H <;> simp [H]