Lemma natsummationreindexing { R : commring } { upper : nat } ( i : nat -> nat ) ( p : isnattruncauto upper i ) ( f : nat -> R ) : natsummation0 upper f = natsummation0 upper (funcomp i f ). Proof. revert i p f. induction upper. - intros. simpl. assert ( 0%nat = i 0%nat ) as f0. { destruct ( natlehchoice ( i 0%nat ) 0%nat ( pr2 p 0%nat ( isreflnatleh 0%nat ) ) ) as [ h | k ]. + apply fromempty. exact ( negnatlthn0 ( i 0%nat ) h ). + rewrite k. apply idpath. } rewrite <- f0. apply idpath. - intros. simpl ( natsummation0 ( S upper ) f ). set ( j := nattruncautopreimagepath p ( isreflnatleh ( S upper ) ) ). set ( v := nattruncautopreimage p ( isreflnatleh ( S upper ) ) ). change ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) with v in j. destruct ( natlehchoice 0%nat v ( natleh0n v ) ) as [ h | p0 ] . + set ( aaa := nattruncautopreimageineq p ( isreflnatleh ( S upper ) ) ). change ( nattruncautopreimage p ( isreflnatleh ( S upper ) ) ) with v in aaa. destruct ( natlehchoice v ( S upper ) aaa ) as [ l | r ]. * rewrite ( IHupper ( funcomp ( natcoface v ) i ) ). -- change ( funcomp ( funcomp ( natcoface v ) i ) f ) with ( funcomp ( natcoface v ) ( funcomp i f ) ). assert ( f ( S upper ) = ( funcomp i f ) v ) as f0. { simpl. rewrite j. apply idpath. } rewrite f0. assert ( natleh v upper ) as aux. { apply natlthsntoleh. assumption. } rewrite ( natsummationshift upper ( funcomp i f ) aux ). apply idpath. -- apply precompwithnatcofaceisauto. assumption. * rewrite ( IHupper ( funcomp ( natcoface v ) i ) ). -- assert ( natsummation0 upper ( funcomp ( funcomp ( natcoface v ) i) f ) = natsummation0 upper ( funcomp i f ) ) as f0. { apply natsummationpathsupperfixed. intros x X. simpl. unfold natcoface. assert ( natlth x v ) as a0. { apply ( natlehlthtrans _ upper ). ++ assumption. ++ rewrite r. apply natlthnsn. } rewrite a0. apply idpath. } rewrite f0. assert ( f ( S upper ) = funcomp i f ( S upper ) ) as f1. { simpl. rewrite <- r. rewrite j. rewrite <- r. apply idpath. } rewrite f1. apply idpath. -- apply precompwithnatcofaceisauto. assumption. + rewrite natsummationshift0. simpl. rewrite p0. rewrite j. assert ( i 0%nat = S upper ) as j'. { rewrite p0. rewrite j. apply idpath. } rewrite ( IHupper ( funcomp S i ) ( isnattruncauto0S p j' ) ). apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.