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