Lemma iscotransafldfracapartrelpre : iscotrans afldfracapartrelpre. Proof. 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 ( a * f * d # e * b * d ) as v. { apply azerormultcomp; assumption. } use (hinhuniv _ ( acommring_acotrans A ( a * f * d ) ( c * b * f ) ( e * b * d ) v )). intro u. intros P k. apply k. unfold afldfracapartrelpre in *. simpl in *. destruct u as [ left | right ]. - apply ii1. apply ( pr2 ( acommring_amult A ) f ). assert ( @op2 A ( @op2 A a f ) d = @op2 A ( @op2 A a d ) f ) as i by permute. change ( @op2 A ( @op2 A a d ) f # @op2 A ( @op2 A c b ) f ). rewrite <- i. assumption. - apply ii2. apply ( pr2 ( acommring_amult A ) b ). assert ( @op2 A ( @op2 A c f ) b = @op2 A ( @op2 A c b ) f ) as i by permute. change ( @op2 A ( @op2 A c f ) b # @op2 A ( @op2 A e d ) b ). rewrite i. assert ( @op2 A ( @op2 A e d ) b = @op2 A ( @op2 A e b ) d ) as j by permute. change ( @op2 A ( @op2 A c b ) f # @op2 A ( @op2 A e d ) b ). rewrite j. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.