proposition: Lemma hzqrandcarryeq ( a : fpscommring hz ) ( n : nat ) : carry a n = m * 0 + carry a n.
proof: Proof. intros. rewrite hzmultx0. rewrite hzplusl0. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers