theorem MyRing.add_zero {R : Type u_1} [Ring R] (a : R) : a + 0 = a

theorem MyRing.add_right_neg {R : Type u_1} [Ring R] (a : R) : a + -a = 0

theorem MyRing.neg_add_cancel_left {R : Type u_1} [Ring R] (a : R) (b : R) : -a + (a + b) = b

theorem MyRing.add_neg_cancel_right {R : Type u_1} [Ring R] (a : R) (b : R) : a + b + -b = a

theorem MyRing.add_left_cancel {R : Type u_1} [Ring R] {a : R} {b : R} {c : R} (h : a + b = a + c) : b = c

theorem MyRing.add_right_cancel {R : Type u_1} [Ring R] {a : R} {b : R} {c : R} (h : a + b = c + b) : a = c

theorem MyRing.mul_zero {R : Type u_1} [Ring R] (a : R) : a * 0 = 0

theorem MyRing.zero_mul {R : Type u_1} [Ring R] (a : R) : 0 * a = 0

theorem MyRing.neg_eq_of_add_eq_zero {R : Type u_1} [Ring R] {a : R} {b : R} (h : a + b = 0) : -a = b

theorem MyRing.eq_neg_of_add_eq_zero {R : Type u_1} [Ring R] {a : R} {b : R} (h : a + b = 0) : a = -b

theorem MyRing.neg_zero {R : Type u_1} [Ring R] : -0 = 0

theorem MyRing.neg_neg {R : Type u_1} [Ring R] (a : R) : - -a = a

theorem MyRing.self_sub {R : Type u_1} [Ring R] (a : R) : a - a = 0

theorem MyRing.one_add_one_eq_two {R : Type u_1} [Ring R] : 1 + 1 = 2

theorem MyRing.two_mul {R : Type u_1} [Ring R] (a : R) : 2 * a = a + a

theorem MyGroup.mul_inv_cancel {G : Type u_1} [Group G] (a : G) : a * a⁻¹ = 1

theorem MyGroup.mul_one {G : Type u_1} [Group G] (a : G) : a * 1 = a

theorem MyGroup.mul_inv_rev {G : Type u_1} [Group G] (a : G) (b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹