Definition fpsshift { R : commring } ( a : fpscommring R ) : fpscommring R := fun n : nat => a ( S n ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.