Lemma isbinapartlafldfracop1 : isbinopapartl afldfracapart op1. Proof. intros. unfold isbinopapartl. assert ( forall a b c : commringfrac A ( aintdomazerosubmonoid A ), isaprop ( pr1 (afldfracapart) ( commringfracop1 A ( aintdomazerosubmonoid A ) a b) ( commringfracop1 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' ]. unfold afldfracapart in *. simpl. unfold afldfracapartrel. unfold quotrel. rewrite setquotuniv2comm. unfold afldfracapartrelpre. simpl. assert ( afldfracapartrelpre ( make_dirprod ( @op1 A ( @op2 A d a ) ( @op2 A b c ) ) ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair d d' ) ) ) ( make_dirprod ( @op1 A ( @op2 A f a ) ( @op2 A b e ) ) ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair f f' ) ) ) ) as u by apply p. unfold afldfracapartrelpre in u. simpl in u. rewrite 2! ( @ringrdistr A ) in u. do 4 rewrite <- ringassoc2 in u. assert ( (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) d a) b) f) = (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) f a) b) d) ) as i by permute. rewrite i in u. assert ( (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) b c) b) f) = (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) c f) b) b) ) as j by permute. rewrite j in u. assert ( (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) b e) b) d) = (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A)))) (@op2 (@pr1 setwith2binop (fun X : setwith2binop => @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X)) (acommringtocommring (pr1aintdom A))) e d) b) b) ) as j' by permute. rewrite j' in u. apply ( pr2 ( acommring_amult A ) b ). apply ( pr2 ( acommring_amult A ) b ). apply ( pr1 ( acommring_aadd A) ( f * a * b * d ) ). assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.