proposition: Lemma carryandcarryequiv ( a : fpscommring hz ) : carryequiv ( carry a ) a.
proof: Proof. intros. simpl. rewrite doublecarry. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers