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