Definition fpstimes ( R : commring ) : binop ( fps R ) := fun s t n => natsummation0 n ( fun x : nat => s x * t ( sub n x ) ). Local Definition test0 : seqson hz. Proof. intro n. induction n. - exact 0. - exact ( nattohz ( S n ) ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.