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