Lemma hzqrandcarryr ( a : fpscommring hz ) ( n : nat ) : carry a n = hzremaindermod m is ( carry a n ). Proof. intros. apply ( hzqrtestr m is ( carry a n ) 0 ( carry a n ) ). split. - apply hzqrandcarryeq. - apply hzqrandcarryineq. Defined.
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.