Lemma fpsapartisbinopapartmultl ( R : acommring ) : isbinopapartl ( fpsapart R ) ( @op2 ( fpsring R ) ). Proof. intros. intros a b c p. intros P s. use (hinhuniv _ p). intro k. destruct k as [ n q ]. change ( ( a * b ) n ) with ( natsummation0 n ( fun x : nat => a x * b ( sub n x ) ) ) in q. change ( ( a * c ) n ) with ( natsummation0 n ( fun x : nat => a x * c ( sub n x ) ) ) in q. assert ( natsummation0 n ( fun x : nat => ( a x * b ( sub n x ) - ( a x * c ( sub n x ) ) ) ) # 0 ) as q'. { assert ( natsummation0 n ( fun x : nat => ( a x * b ( sub n x ) ) ) - natsummation0 n ( fun x : nat => ( a x * c ( sub n x ) ) ) # 0 ) as q''. { apply aaminuszero. assumption. } assert ( (fun x : nat => a x * b (sub n x) - a x * c ( sub n x)) = (fun x : nat => a x * b ( sub n x) + ( - 1%ring ) * ( a x * c ( sub n x)) ) ) as i. { apply funextfun. intro x. apply maponpaths. rewrite <- ( ringmultwithminus1 R ). apply idpath. } rewrite i. rewrite natsummationplusdistr. rewrite <- ( natsummationtimesdistr n ( fun x : nat => a x * c ( sub n x ) ) ( - 1%ring ) ). rewrite ( ringmultwithminus1 R ). assumption. } use ( hinhuniv _ ( apartnatsummation0 R n _ q' ) ). intro k. destruct k as [ m g ]. destruct g as [ g g' ]. apply s. split with ( sub n m ). apply ( pr1 ( acommring_amult R ) ( a m ) ( b ( sub n m ) ) ( c ( sub n m ) ) ). apply aminuszeroa. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.