proposition: Theorem add_mult_div_2: forall w, [|w_add_mul_div (w_pred w_zdigits) w_0 w|] = [|w|] / 2.
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. rewrite spec_w_add_mul_div by zarith. autorewrite with w_rewrite rm10. match goal with |- context[?X - ?Y] => replace (X - Y) with 1 end. rewrite Z.pow_1_r. rewrite Zmod_small. zarith. destruct (spec_to_Z w1) as [H1 H2]. split. zarith. apply Zdiv_lt_upper_bound; zarith. rewrite Hp; ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase