Lemma afldfracapartiscomprel : iscomprelrel ( eqrelcommringfrac A ( aintdomazerosubmonoid A ) ) ( afldfracapartrelpre ). Proof. intros ab cd ef gh p q. unfold afldfracapartrelpre. 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' ]. destruct gh as [ g h ]. destruct h as [ h h' ]. simpl in *. apply hPropUnivalence. - intro u. apply p. intro p'. apply q. intro q'. destruct p' as [ p' j ]. destruct p' as [ i p' ]. destruct q' as [ q' j']. destruct q' as [ i' q' ]. simpl in *. assert ( a * f * d * i * h * i' # e * b * d * i * h * i') as v0. { assert ( a * f * d # e * b * d ) as v0. { apply azerormultcomp. + apply d'. + assumption. } assert ( a * f * d * i # e * b * d * i ) as v1 by (apply azerormultcomp; assumption). assert ( a * f * d * i * h # e * b * d * i * h ) as v2 by (apply azerormultcomp; assumption). apply azerormultcomp; assumption. } apply ( pr2 ( acommring_amult A ) b ). apply ( pr2 ( acommring_amult A ) f ). apply ( pr2 ( acommring_amult A ) i ). apply ( pr2 ( acommring_amult A ) i' ). assert ( a * f * d * i * h * i' = c * h * b * f * i * i' ) as l. { assert ( a * f * d * i * h * i' = a * d * i * f * h * i' ) as l0. { change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a f ) d ) i ) h ) i' = @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a d ) i ) f ) h ) i' ). permute. } rewrite l0. rewrite j. change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c b ) i ) f ) h ) i' = @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c h ) b ) f ) i ) i' ). permute. } rewrite l in v0. assert ( e * b * d * i * h * i' = g * d * b * f * i * i' ) as k. { assert ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e b ) d ) i ) h ) i' = @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e h ) i' ) i ) b ) d ) as k0 by permute. change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e b ) d ) i ) h ) i' = @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A g d ) b ) f ) i ) i' ). rewrite k0. assert ( @op2 A ( @op2 A e h ) i' = @op2 A ( @op2 A g f ) i' ) as j'' by assumption. rewrite j''. permute. } rewrite k in v0. assumption. - intro u. apply p. intro p'. apply q. intro q'. destruct p' as [ p' j ]. destruct p' as [ i p' ]. destruct q' as [ q' j' ]. destruct q' as [ i' q' ]. simpl in *. assert ( c * h * b * f * i * i' # g * d * b * f * i * i' ) as v. { apply azerormultcomp. + apply q'. + apply azerormultcomp. * apply p'. * apply azerormultcomp. -- apply f'. -- apply azerormultcomp. ++ apply b'. ++ assumption. } apply ( pr2 ( acommring_amult A ) d ). apply ( pr2 ( acommring_amult A ) h ). apply ( pr2 ( acommring_amult A ) i ). apply ( pr2 ( acommring_amult A ) i' ). assert ( c * h * b * f * i * i' = a * f * d * h * i * i' ) as k. { assert ( c * h * b * f * i * i' = c * b * i * f * h * i' ) as k0. { change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c h ) b ) f ) i ) i' = @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c b ) i ) f ) h ) i' ). permute. } rewrite k0. rewrite <- j. change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a d ) i ) f ) h ) i' = @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a f ) d ) h ) i ) i' ). permute. } rewrite k in v. assert ( g * d * b * f * i * i' = e * b * d * h * i * i' ) as l. { assert ( g * d * b * f * i * i' = g * f * i' * d * i * b ) as l0. { change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A g d ) b ) f ) i ) i' = @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A g f ) i' ) d ) i ) b ). permute. } rewrite l0. rewrite <- j'. change (@op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e h ) i' ) d ) i ) b = @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e b ) d ) h ) i ) i' ). permute. } rewrite l in v. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.