proposition: Lemma wwB_wBwB : wwB = wB^2.
proof: Proof. unfold base, ww_digits;rewrite Z.pow_2_r; rewrite (Pos2Z.inj_xO w_digits). replace (2 * Zpos w_digits) with (Zpos w_digits + Zpos w_digits). apply Zpower_exp; unfold Z.ge;simpl;intros;discriminate. ring. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType