Lemma natsummationplusdistr { R : commring } ( upper : nat ) ( f g : nat -> R ) : natsummation0 upper ( fun x : nat => f x + g x ) = natsummation0 upper f + natsummation0 upper g. Proof. revert f g. induction upper. - auto. - intros f g. simpl. rewrite <- ( ringassoc1 R _ ( natsummation0 upper g ) _ ). rewrite ( ringassoc1 R ( natsummation0 upper f ) ). rewrite ( ringcomm1 R _ ( natsummation0 upper g ) ). rewrite <- ( ringassoc1 R ( natsummation0 upper f ) ). rewrite <- ( IHupper f g ). rewrite ( ringassoc1 R ). apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.