proposition: Lemma to_ring_zero_sum x y : -f x = f y → x = 0 ∧ y = 0.
proof: Proof. intros E. apply zero_sum, (injective f). rewrite rings.preserves_0, rings.preserves_plus, <-E. now apply plus_negate_r. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.implementations.peano_naturals MathClasses.theory.rings Coq.Arith.PeanoNat MathClasses.categories.varieties MathClasses.theory.ua_transference MathClasses.interfaces.naturals