proposition: Lemma multinvmultstable ( A : commring ) ( a b : A ) ( p : multinvpair A a ) ( q : multinvpair A b ) : multinvpair A ( a * b ).
proof: 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.
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