fact: Definition carry : fpscommring hz -> fpscommring hz := fun (a : fpscommring hz) (n : nat) => hzremaindermod m is ( precarry a n ).
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers