Definition quotientprecarry ( a : fpscommring hz ) : fpscommring hz := fun x : nat => hzquotientmod m is ( precarry a x ).
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.