proposition: Theorem ww_add_mult_mult_2_plus_1: forall w, [[ww_add_mul_div (w_0W w_1) w wwBm1]] = (2 * [[w]] + 1) mod wwB.
proof: Proof. intros w1. rewrite spec_ww_add_mul_div; rewrite spec_w_0W; rewrite spec_w_1. 2: lia. rewrite Z.pow_1_r. f_equal. rewrite Z.mul_comm; f_equal. autorewrite with w_rewrite rm10. unfold ww_digits, base. symmetry; apply Zdiv_unique with (r := 2 ^ (Zpos (ww_digits w_digits) - 1) -1). { unfold ww_digits; split. 2: lia. match goal with |- 0 <= ?X - 1 => enough (0 < X) by lia end. apply Z.pow_pos_nonneg; lia. } unfold ww_digits; autorewrite with rm10. assert (tmp: forall p q r, p + (q - r) = p + q - r) by zarith; rewrite tmp; clear tmp. assert (tmp: forall p, p + p = 2 * p) by zarith; rewrite tmp; clear tmp. f_equal; auto. pattern 2 at 2; rewrite <- Z.pow_1_r; rewrite <- Zpower_exp by lia. assert (tmp: forall p, 1 + (p - 1) = p) by zarith; rewrite tmp; clear tmp; auto. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase