Lemma isldistrfps ( R : commring ) ( s t u : fps R ) : fpstimes R s ( fpsplus R t u ) = fpsplus R ( fpstimes R s t ) ( fpstimes R s u ). Proof. intros. unfold fpstimes. unfold fpsplus. change ((fun n : nat => natsummation0 n (fun x : nat => s x * (t (sub n x) + u ( sub n x)))) = (fun n : nat => natsummation0 n (fun x : nat => s x * t (sub n x)) + natsummation0 n (fun x : nat => s x * u (sub n x)))). apply funextfun. intro upper. assert ( natsummation0 upper ( fun x : nat => s x * ( t ( sub upper x ) + u ( sub upper x ) ) ) = natsummation0 upper ( fun x : nat => ( ( s x * t ( sub upper x ) ) + ( s x * u ( sub upper x ) ) ) ) ) as a0. { apply maponpaths. apply funextfun. intro n. apply R. } assert ( natsummation0 upper ( fun x : nat => ( ( s x * t ( sub upper x ) ) + ( s x * u ( sub upper x ) ) ) ) = natsummation0 upper ( fun x : nat => s x * t ( sub upper x ) ) + natsummation0 upper ( fun x : nat => s x * u ( 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.