Lemma precarryandzeromult ( a b : fpscommring hz ) ( k k' : nat ) ( x : forall m : nat, natlth m k -> carry p ( isaprimetoneq0 is ) a m = 0%hz ) ( x' : forall m : nat, natlth m k' -> carry p ( isaprimetoneq0 is ) b m = 0%hz ) : forall m : nat, natlth m ( k + k' )%nat -> precarry p ( isaprimetoneq0 is ) ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) m = 0%hz. Proof. intros m i. induction m. - apply ( hzfpstimeswhenzero ( carry p ( isaprimetoneq0 is ) a ) 0%nat k x ( carry p ( isaprimetoneq0 is ) b ) k' x' i ). - change ( ( ( carry p ( isaprimetoneq0 is ) a ) * ( carry p ( isaprimetoneq0 is ) b ) ) ( S m ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) m ) = 0%hz ). rewrite ( hzfpstimeswhenzero ( carry p ( isaprimetoneq0 is ) a ) ( S m ) k x ( carry p ( isaprimetoneq0 is ) b ) k' x' i ). rewrite hzplusl0. assert ( natlth m ( k + k' )%nat ) as one. { apply ( istransnatlth _ ( S m ) _ ). + apply natlthnsn. + assumption. } rewrite ( IHm one ). rewrite hzqrand0q. 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.