proposition: 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: 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.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers