proposition: Theorem wwB_div: wwB = 2 * (wwB / 2).
proof: Proof. rewrite wwB_div_2; rewrite Z.mul_assoc; rewrite wB_div_2; auto. rewrite <- Z.pow_2_r; apply wwB_wBwB. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub