Lemma precarryandzeromultl ( a b : fpscommring hz ) ( n : nat ) ( x : forall m : nat, natlth m n -> carry p ( isaprimetoneq0 is ) a 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. induction m. - simpl. unfold fpstimes. simpl. rewrite ( x 0%nat y ). rewrite hzmult0x. apply idpath. - change ( natsummation0 ( S m ) ( fun z : nat => ( carry p ( isaprimetoneq0 is ) a z ) * ( carry p ( isaprimetoneq0 is ) b ( sub ( S m ) z ) ) ) + hzquotientmod p ( isaprimetoneq0 is ) ( precarry p ( isaprimetoneq0 is ) ( fpstimes hz ( carry p ( isaprimetoneq0 is ) a ) ( carry p ( isaprimetoneq0 is ) b ) ) m ) = 0%hz ). assert ( natlth m n ) as u. + apply ( istransnatlth _ ( S m ) _ ). { apply natlthnsn. } assumption. + rewrite ( IHm u ). rewrite hzqrand0q. rewrite hzplusr0. assert ( natsummation0 (S m) (fun z : nat => carry p (isaprimetoneq0 is) a z * carry p (isaprimetoneq0 is) b ( sub ( S m ) z)) = natsummation0 ( S m ) ( fun z : nat => 0%hz ) ) as f. { apply natsummationpathsupperfixed. intros k v. assert ( natlth k n ) as uu. * apply ( natlehlthtrans _ ( S m ) _ ); assumption. * rewrite ( x k uu ). rewrite hzmult0x. apply idpath. } rewrite f. rewrite natsummationae0bottom. * apply idpath. * intros k l. 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.