Lemma multinvmultstable ( A : commring ) ( a b : A ) ( p : multinvpair A a ) ( q : multinvpair A b ) : multinvpair A ( a * b ). Proof. intros. destruct p as [ a' p ]. destruct q as [ b' q ]. split with ( b' * a' ). split. - change ( ( ( b' * a' ) * ( a * b ) )%ring = @ringunel2 A ). rewrite ( ringassoc2 A b'). rewrite <- ( ringassoc2 A a' ). change ( ( ( a' * a )%ring = @ringunel2 A ) × ( ( a * a' )%ring = @ringunel2 A ) ) in p. change ( ( ( b' * b )%ring = @ringunel2 A ) × ( ( b * b' )%ring = @ringunel2 A ) ) in q. rewrite <- ( pr1 q ). apply maponpaths. assert ( a' * a * b = 1 * b ) as f by apply ( maponpaths ( fun x => x * b ) ( pr1 p ) ). rewrite ringlunax2 in f. assumption. - change ( ( ( a * b ) * ( b' * a' ) )%ring = @ringunel2 A ). rewrite ( ringassoc2 A a). rewrite <- ( ringassoc2 A b ). change ( ( ( a' * a )%ring = @ringunel2 A ) × ( ( a * a' )%ring = @ringunel2 A ) ) in p. change ( ( ( b' * b )%ring = @ringunel2 A ) × ( ( b * b' )%ring = @ringunel2 A ) ) in q. rewrite <- ( pr2 q ). rewrite ( pr2 q ). rewrite ringlunax2. apply (pr2 p). 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.