fact: Definition quotientprecarry ( a : fpscommring hz ) : fpscommring hz := fun x : nat => hzquotientmod m is ( precarry a x ).
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers