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