Definition fpsapart0 ( R : acommring ) : hrel ( fpscommring R ) := fun s t : fpscommring R => ∃ n : nat, s n # t n.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.