proposition: Lemma isapropcarryequiv ( a b : fpscommring hz ) : isaprop ( carry a = carry b ).
proof: Proof. intros. apply ( fps hz ). Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers