Lemma isbinapartlafldfracop2 : isbinopapartl afldfracapart op2. Proof. intros. unfold isbinopapartl. assert ( forall a b c : commringfrac A ( aintdomazerosubmonoid A ), isaprop ( pr1 (afldfracapart ) ( commringfracop2 A ( aintdomazerosubmonoid A ) a b) ( commringfracop2 A ( aintdomazerosubmonoid A ) a c) -> pr1 (afldfracapart ) b c) ) as int. { intros a b c. apply impred. intro p. apply ( pr1 ( afldfracapart ) b c ). } apply ( setquotuniv3prop _ ( fun a b c => make_hProp _ ( int a b c ) ) ). intros ab cd ef p. destruct ab as [ a b ]. destruct b as [ b b' ]. destruct cd as [ c d ]. destruct d as [ d d' ]. destruct ef as [ e f ]. destruct f as [ f f' ]. assert ( afldfracapartrelpre ( make_dirprod ( ( a * c ) ) ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair d d' ) ) ) ( make_dirprod ( a * e ) ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair f f' ) ) ) ) as u by apply p. unfold afldfracapart in *. simpl. unfold afldfracapartrel. unfold quotrel. rewrite ( setquotuniv2comm ( eqrelcommringfrac A ( aintdomazerosubmonoid A ) ) ). unfold afldfracapartrelpre in *. simpl. simpl in u. apply ( pr2 ( acommring_amult A ) a ). apply ( pr2 ( acommring_amult A ) b ). assert ( c * f * a * b = (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) a c) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) b f)) ) as i. { change ( c * f * a * b = a * c * ( b * f ) ). permute. } change ( c * f * a * b # e * d * a * b ). rewrite i. assert ( e * d * a * b = (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) a e) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) b d)) ) as i'. { change ( e * d * a * b = a * e * ( b * d ) ). permute. } rewrite i'. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.