proposition: Lemma zero_sum (x y : N) : x + y = 0 → x = 0 ∧ y = 0.
proof: Proof. rapply (from_nat_stmt (x' + y' === 0 -=> Conj _ (x' === 0) (y' === 0)) (two_vars x y)). intro. simpl. apply Nat.eq_add_0. 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