Lemma precarryandcarry ( a : fpscommring hz ) : precarry ( carry a ) = carry a. Proof. intros. apply funextfun. intro n. apply precarryandcarry_pointwise. 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.