theorem add_sub_comm' (a b c : ℝ) : a + b - c = a - c + b

theorem sub_eq_neg_sub_inv {a b : ℝ} : a - b = -(b - a)

theorem square_diff {a b : ℝ} : a ^ 2 - b ^ 2 = (a - b) * (a + b)