Lemma natsummationae0top { R : commring } { f : nat -> R } ( upper : nat ) ( p : forall x : nat, natlth x upper -> f x = 0 ) : natsummation0 upper f = f upper. Proof. revert p. induction upper. - auto. - intro p. assert ( natsummation0 upper f = natsummation0 ( R := R ) upper ( fun x : nat => 0 ) ) as g. { apply natsummationpathsupperfixed. intros m q. apply p. exact ( natlehlthtrans m upper ( S upper ) q ( natlthnsn upper ) ). } simpl. rewrite g. assert ( natsummation0 ( R := R ) upper ( fun _ : nat => 0 ) = 0 ) as g'. { set ( g'' := fun x : nat => ringunel1 ( X := R ) ). assert ( forall x : nat, natlth 0 x -> g'' x = 0 ) as q0. { intros k pp. apply idpath. } exact ( natsummationae0bottom upper q0 ). } rewrite g'. rewrite ( ringlunax1 R ). apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.