proposition: 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: 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.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers