proposition: Theorem add_mult_mult_2: forall w, [|w_add_mul_div w_1 w w_0|] = 2 * [|w|] mod wB.
proof: Proof. intros w1. autorewrite with w_rewrite rm10. 2: zarith. rewrite Z.mul_comm; auto. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase