proposition: Lemma precarryandcarry_pointwise ( a : fpscommring hz ) : forall n : nat, precarry ( carry a ) n = ( carry a ) n.
proof: Proof. intros. induction n. - exact (idpath _). - unfold precarry. fold precarry. rewrite IHn. unfold carry at 2. rewrite <- hzqrandremainderq. apply hzplusr0. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers