lean_problem_sheets / 2020.problem_sheets.Part_II_sheet1

theorem Q1a (x y : ℕ) :

x + y = y + x

Note: this declaration is incomplete and uses sorry.

theorem Q1b (x y : ℕ) :

x + y = x → y = 0

Note: this declaration is incomplete and uses sorry.

theorem Q1c (x y : ℕ) :

x + y = 0 → x = 0 ∧ y = 0

Note: this declaration is incomplete and uses sorry.

theorem Q1d (x y : ℕ) :

x * y = y * x

Note: this declaration is incomplete and uses sorry.