Definition fpsone ( R : commring ) : fps R. Proof. intros. intro n. destruct n. - exact 1. - exact 0. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.