proposition: Lemma aminuszeroa { A : acommring } { a b : A } ( p : ( a - b ) # 0 ) : a # b.
proof: Proof. intros. change 0 with ( @ringunel1 A ) in p. rewrite <- ( ringrinvax1 A b ) in p. rewrite <- ( ringmultwithminus1 A ) in p. apply ( pr2 ( acommring_aadd A ) ( -1 * b ) a b ). assumption. Defined.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids