Definition fpsplus ( R : commring ) : binop ( fps R ) := fun v w n => ( ( v n ) + ( w n ) ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.