proposition: Lemma mod_wwB : forall z x, (z*wB + [|x|]) mod wwB = (z mod wB)*wB + [|x|].
proof: Proof. intros z x. rewrite Zplus_mod. pattern wwB at 1;rewrite wwB_wBwB; rewrite Z.pow_2_r. rewrite Zmult_mod_distr_r;try apply lt_0_wB. rewrite (Zmod_small [|x|]). apply Zmod_small;rewrite wwB_wBwB;apply beta_mult;try apply spec_to_Z. apply Z_mod_lt;apply Z.lt_gt;apply lt_0_wB. destruct (spec_to_Z x);split;trivial. change [|x|] with (0*wB+[|x|]). rewrite wwB_wBwB. rewrite Z.pow_2_r;rewrite <- (Z.add_0_r (wB*wB));apply beta_lex_inv. apply lt_0_wB. apply spec_to_Z. split;[apply Z.le_refl | apply lt_0_wB]. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType