proposition: Lemma wwB_pos: 1 < wwB.
proof: Proof. assert (H:= wB_pos);rewrite wwB_wBwB;rewrite <-(Z.mul_1_r 1). rewrite Z.pow_2_r. apply Zmult_lt_compat2;(split;[unfold Z.lt;reflexivity|trivial]). apply Z.lt_le_incl;trivial. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType