Lemma aaminuszero { A : acommring } { a b : A } ( p : a # b ) : ( a - b ) # 0. 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.