Lemma precarryandzeromultr ( a b : fpscommring hz ) ( n : nat ) ( x : forall m : nat, natlth m n -> carry p ( isaprimetoneq0 is ) b m = 0%hz ) : forall m : nat, natlth m n -> precarry p ( isaprimetoneq0 is ) ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) m = 0%hz. Proof. intros m y. change (fpstimes hz (carry p (isaprimetoneq0 is) a) (carry p (isaprimetoneq0 is) b)) with ( (carry p (isaprimetoneq0 is) a) * (carry p (isaprimetoneq0 is) b)). rewrite ( @ringcomm2 ( fpscommring hz ) ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ). apply ( precarryandzeromultl b a n x m y ). 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.