Lemma natsummationshift { R : commring } ( upper : nat ) ( f : nat -> R ) { i : nat } ( p : natleh i upper ) : natsummation0 ( S upper ) f = natsummation0 upper ( funcomp ( natcoface i ) f ) + f i. Proof. revert f i p. induction upper. - intros f i p. destruct i. + unfold natcoface. 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. + apply fromempty. exact ( negnatlehsn0 i p ). - intros f i p. destruct i. + apply natsummationshift0. + destruct ( natlehchoice ( S i ) ( S upper ) p ) as [ h | k ]. * change ( natsummation0 ( S upper ) f + f ( S ( S upper ) ) = natsummation0 ( S upper ) ( funcomp ( natcoface ( S i ) ) f ) + f ( S i ) ). rewrite ( IHupper f ( S i ) ). -- simpl. unfold natcoface at 3. rewrite 2! ( ringassoc1 R ). rewrite ( ringcomm1 R _ ( f ( S i ) ) ). simpl. rewrite ( natgehimplnatgtbfalse i upper ). ++ apply idpath. ++ apply p. -- apply natlthsntoleh. assumption. * simpl. assert ( natsummation0 upper ( funcomp ( natcoface ( S i ) ) f ) = natsummation0 upper f ) as h. { apply natsummationpathsupperfixed. intros m q. unfold natcoface. assert ( natlth m ( S i ) ) as q'. { apply ( natlehlthtrans _ upper ). -- assumption. -- rewrite k. apply natlthnsn. } unfold natlth in q'. unfold funcomp. rewrite q'. apply idpath. } rewrite <- h. unfold natcoface at 3. simpl. rewrite ( natgehimplnatgtbfalse i upper ). -- rewrite 2! ( ringassoc1 R ). rewrite ( ringcomm1 R ( f ( S ( S upper ) ) ) ). rewrite k. apply idpath. -- apply p. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.