Definition natsummation0 { R : commring } ( upper : nat ) ( f : nat -> R ) : R. Proof. revert f. induction upper. - intros. exact ( f 0%nat ). - intros. exact ( IHupper f + f ( S upper ) ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.