proposition: Lemma carryandtimes ( a b : fpscommring hz ) : carry ( a * b ) = carry ( carry a * carry b ).
proof: Proof. intros. rewrite carryandtimesl. rewrite carryandtimesr. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers