fact: Definition fpstimes ( R : commring ) : binop ( fps R ) := fun s t n => natsummation0 n ( fun x : nat => s x * t ( sub n x ) ).
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers