Lemma natsummationtimesdistr { R : commring } ( upper : nat ) ( f : nat -> R ) ( k : R ) : k * ( natsummation0 upper f ) = natsummation0 upper ( fun x : nat => k * f x ). Proof. revert f k. induction upper. - auto. - intros f k. simpl. rewrite <- IHupper. rewrite <- ( ringldistr R ). apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.