Definition carryequiv0 : hrel ( fpscommring hz ) := fun a b : fpscommring hz => make_hProp _ ( isapropcarryequiv a b ).
Require Import UniMath.PAdics.lemmas. Require Import UniMath.PAdics.fps. Require Import UniMath.PAdics.frac. Require Import UniMath.PAdics.z_mod_p. Require Import UniMath.NumberSystems.Integers.