no goals
m n k l : ℕ
⊢ m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0
cases n <;>
simp [(succ_ne_zero 1).symm, (show 2 = Nat.succ 1 from rfl),
  succ_eq_add_one, ← add_assoc, succ_inj', add_eq_one_iff]