proposition: Theorem wwB_div_2 : wwB / 2 = wB / 2 * wB.
proof: Proof. clear spec_w_0 w_0 spec_w_1 w_1 spec_w_Bm1 w_Bm1 spec_w_WW spec_w_0W spec_to_Z. rewrite wwB_wBwB; rewrite Z.pow_2_r. pattern wB at 1; rewrite <- wB_div_2; auto. rewrite <- Z.mul_assoc. repeat (rewrite (Z.mul_comm 2); rewrite Z_div_mult); auto with zarith. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType