Lemma natsummationplusshift { R : commring } ( upper : nat ) ( f g : nat -> R ) : natsummation0 ( S upper ) f + natsummation0 upper g = f 0%nat + natsummation0 upper ( fun x : nat => f ( S x ) + g x ). Proof. intros. destruct upper. - unfold natsummation0. simpl. apply ( ringassoc1 R ). - rewrite (natsummationshift0 ( S upper ) f ). rewrite ( ringcomm1 R _ ( f 0%nat ) ). rewrite ( ringassoc1 R ). rewrite natsummationplusdistr. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.PAdics.fps. Require Import UniMath.PAdics.frac. Require Import UniMath.PAdics.z_mod_p. Require Import UniMath.NumberSystems.Integers.