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