proposition: Theorem mmul_aux3:forall xh xl, [[WW xh xl]] mod (2 ^ Zpos p) = [|xl|] mod (2 ^ Zpos p).
proof: Proof. intros xh xl; simpl ww_to_Z; unfold base. rewrite Zplus_mod; auto with zarith. generalize mmul_aux1; unfold w_digits; intros tmp; rewrite tmp; clear tmp. rewrite Zmult_assoc. rewrite Z_mod_mult; auto with zarith. rewrite Zplus_0_l; apply Zmod_mod; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux