proposition: Lemma precarryandcarry ( a : fpscommring hz ) : precarry ( carry a ) = carry a.
proof: Proof. intros. apply funextfun. intro n. apply precarryandcarry_pointwise. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers