proposition: Theorem ww_add_mult_mult_2: forall w, [[ww_add_mul_div (w_0W w_1) w W0]] = 2 * [[w]] mod wwB.
proof: Proof. intros w1. rewrite spec_ww_add_mul_div. autorewrite with w_rewrite rm10. rewrite spec_w_0W; rewrite spec_w_1. rewrite Z.pow_1_r by zarith. rewrite Z.mul_comm; easy. rewrite spec_w_0W; rewrite spec_w_1. red; simpl; intros; discriminate. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase