Lemma natsummationshift0 { R : commring } ( upper : nat ) ( f : nat -> R ) : natsummation0 ( S upper ) f = ( natsummation0 upper ( fun x : nat => f ( S x ) ) + f 0%nat ). Proof. revert f. induction upper. - intros f. simpl. set (H:=pr2 R). simpl in H. set (H1:=pr1 H). set (H2:=pr1 H1). set (H3:=pr1 H2). set (H4:=pr2 H3). simpl in H4. apply H4. - intros. change ( natsummation0 ( S upper ) f + f ( S ( S upper ) ) = ( natsummation0 upper ( fun x : nat => f ( S x ) ) + f ( S ( S upper ) ) + f 0%nat ) ). rewrite IHupper. rewrite 2! ( ringassoc1 R ). rewrite ( ringcomm1 R ( f 0%nat ) _ ). apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.