proposition: Lemma nat_1_plus_ne_0 x : 1 + x ≠ 0.
proof: Proof. intro E. destruct (zero_sum 1 x E). now apply nat_nontrivial. 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