Lemma natsummationandfpszero ( R : commring ) : forall m : nat, natsummation0 m ( fun x : nat => fpszero R x ) = @ringunel1 R. Proof. intros m. induction m. - apply idpath. - simpl. rewrite IHm. rewrite ( ringlunax1 R ). apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.