Lemma carryandtimesr ( a b : fpscommring hz ) : carry ( a * b ) = carry ( a * carry b ). Proof. intros. rewrite ( @ringcomm2 ( fpscommring hz ) ). rewrite carryandtimesl. rewrite ( @ringcomm2 ( fpscommring hz ) ). apply idpath. 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.