Lemma precarryandcarry_pointwise ( a : fpscommring hz ) : forall n : nat, precarry ( carry a ) n = ( carry a ) n. Proof. intros. induction n. - exact (idpath _). - unfold precarry. fold precarry. rewrite IHn. unfold carry at 2. rewrite <- hzqrandremainderq. apply hzplusr0. 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.