Lemma isrdistrfps ( R : commring ) ( s t u : fps R ) : fpstimes R ( fpsplus R t u ) s = fpsplus R ( fpstimes R t s ) ( fpstimes R u s ). Proof. intros. unfold fpstimes. unfold fpsplus. change ((fun n : nat => natsummation0 n (fun x : nat => (t x + u x) * s ( sub n x ))) = (fun n : nat => natsummation0 n (fun x : nat => t x * s ( sub n x ) ) + natsummation0 n (fun x : nat => u x * s ( sub n x ) ) ) ). apply funextfun. intro upper. assert ( natsummation0 upper ( fun x : nat => ( t x + u x ) * s ( sub upper x ) ) = natsummation0 upper ( fun x : nat => ( t x * s ( sub upper x ) ) + ( u x * s ( sub upper x ) ) ) ) as a0. { apply maponpaths. apply funextfun. intro n. apply R. } assert ( natsummation0 upper ( fun x : nat => ( ( t x * s ( sub upper x ) ) + ( u x * s ( sub upper x ) ) ) ) = natsummation0 upper ( fun x : nat => t x * s ( sub upper x ) ) + natsummation0 upper ( fun x : nat => u x * s ( sub upper x ) ) ) as a1 by apply natsummationplusdistr. exact ( pathscomp0 a0 a1 ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.