proposition: 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: 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.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers