Lemma natsummationae0bottom { R : commring } { f : nat -> R } ( upper : nat ) ( p : forall x : nat, natlth 0 x -> f x = 0 ) : natsummation0 upper f = f 0%nat. Proof. revert p. induction upper. - auto. - intro p. simpl. rewrite IHupper. + rewrite ( p ( S upper ) ). * rewrite ( ringrunax1 R ). apply idpath. * apply ( natlehlthtrans _ upper _ ). -- apply natleh0n. -- apply natlthnsn. + assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.