proposition: Lemma wwB_4_2: 2 * (wwB / 4) = wwB/ 2.
proof: Proof. pattern wwB at 1; rewrite wwB_wBwB; rewrite Z.pow_2_r. rewrite <- wB_div_2. match goal with |- context[(2 * ?X) * (2 * ?Z)] => replace ((2 * X) * (2 * Z)) with ((X * Z) * 4) by ring end. rewrite Z_div_mult by zarith. rewrite Z.mul_assoc; rewrite wB_div_2. rewrite wwB_div_2; ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase