proposition: Theorem add_mult_div_2_plus_1: forall w, [|w_add_mul_div (w_pred w_zdigits) w_1 w|] = [|w|] / 2 + 2 ^ Zpos (w_digits - 1).
proof: Proof. intros w1. assert (Hp: [|w_pred w_zdigits|] = Zpos w_digits - 1). rewrite spec_pred; rewrite spec_w_zdigits. rewrite Zmod_small. zarith. split. zarith. apply Z.lt_le_trans with (Zpos w_digits). zarith. unfold base; apply Zpower2_le_lin; zarith. autorewrite with w_rewrite rm10. 2: zarith. match goal with |- context[?X - ?Y] => replace (X - Y) with 1 end; rewrite Hp; try ring. rewrite Pos2Z.inj_sub_max by zarith. rewrite Z.max_r by zarith. rewrite Z.pow_1_r; rewrite Zmod_small. zarith. destruct (spec_to_Z w1) as [H1 H2]. split. zarith. unfold base. match goal with |- _ < _ ^ ?X => assert (tmp: forall p, 1 + (p - 1) = p) by zarith; rewrite <- (tmp X); clear tmp end. rewrite Zpower_exp by zarith. rewrite Z.pow_1_r. assert (tmp: forall p, 1 + (p -1) - 1 = p - 1) by zarith; rewrite tmp; clear tmp. match goal with |- ?X + ?Y < _ => enough (Y < X) by zarith end. apply Zdiv_lt_upper_bound. zarith. pattern 2 at 2; rewrite <- Z.pow_1_r; rewrite <- Zpower_exp by zarith. assert (tmp: forall p, (p - 1) + 1 = p) by zarith; rewrite tmp; clear tmp; zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase