proposition: Lemma aaminuszero { A : acommring } { a b : A } ( p : a # b ) : ( a - b ) # 0.
proof: Proof. intros. rewrite <- ( ringrunax1 A a ) in p. rewrite <- ( ringrunax1 A b ) in p. assert ( a + 0 = a + ( b - b ) ) as f. { rewrite <- ( ringrinvax1 A b ). apply idpath. } rewrite f in p. rewrite <- ( ringmultwithminus1 A ) in p. rewrite <- ( ringassoc1 A) in p. rewrite ( ringcomm1 A a ) in p. rewrite ( ringassoc1 A b ) in p. rewrite ( ringmultwithminus1 A ) in p. apply ( pr1 ( acommring_aadd A ) b ( a - b ) 0 ). 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