proposition: Theorem wwB_4_wB_4: wwB / 4 = wB / 4 * wB.
proof: Proof. symmetry; apply Zdiv_unique with 0. zarith. rewrite Z.mul_assoc; rewrite wB_div_4. rewrite wwB_wBwB; ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase