Lemma aminuszeroa { A : acommring } { a b : A } ( p : ( a - b ) # 0 ) : a # b. 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.
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.