Lemma natsummationpathsupperfixed { R : commring } { upper : nat } ( f f' : nat -> R ) ( p : forall x : nat, natleh x upper -> f x = f' x ): natsummation0 upper f = natsummation0 upper f'. Proof. revert f f' p. induction upper. - intros f f' p. simpl. apply p. apply isreflnatleh. - intros. simpl. rewrite ( IHupper f f' ). + rewrite ( p ( S upper ) ). * apply idpath. * apply isreflnatleh. + intros x p'. apply p. apply ( istransnatleh(m := upper) ). * assumption. * apply natlthtoleh. apply natlthnsn. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.