proposition: Theorem mmul_aux4:forall x, [[x]] < [|b|] * 2 ^ Zpos p -> match add_mul_div zp1 W0 x with W0 => 0 | WW _ xl2 => [|xl2|] end = [[x]] / 2 ^ Zpos p.
proof: Proof. intros x Hx. assert (Hp: [[zp1]] <= Zpos (xO w_digits)). rewrite zp1_b; rewrite <- p_p1. assert (0 <= Zpos p); auto with zarith. generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub ZnZ.spec_zdigits spec_low W0 x zp1 Hp). unfold add_mul_div; case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite. rewrite Zmult_0_l; rewrite Zplus_0_l. rewrite zp1_b. generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp. rewrite Zmod_small. auto with zarith. split. apply Z_div_pos. auto with zarith. case (spec_ww_to_Z x); auto with zarith. unfold base. apply Zdiv_lt_upper_bound. auto with zarith. rewrite <- Zpower_exp by auto with zarith. apply Z.lt_le_trans with (base (ww_digits (ZnZ.digits w_op))). case (spec_ww_to_Z x); auto with zarith. unfold base; apply Zpower_le_monotone. auto with zarith. split. auto with zarith. assert (0 < Zpos p); auto with zarith. intros w2 w3; rewrite Zmult_0_l; rewrite Zplus_0_l. rewrite zp1_b. generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp. simpl ww_to_Z; rewrite Zmod_small. intros H1; generalize (high_zero (WW w2 w3)); unfold w_digits;intros tmp; simpl fst in tmp; simpl ww_to_Z in tmp. unfold w_to_Z in *. rewrite tmp in H1. auto with zarith. clear tmp. simpl ww_to_Z; rewrite H1; apply Zdiv_lt_upper_bound. auto with zarith. unfold base; rewrite <- Zpower_exp by auto with zarith. apply Z.lt_le_trans with (1 := Hx). apply Z.le_trans with (2 ^ Zpos p * 2 ^ Zpos p). rewrite p_b; apply Zmult_le_compat_r; auto with zarith. rewrite <- Zpower_exp by auto with zarith. apply Zpower_le_monotone; auto with zarith. split. apply Z_div_pos. auto with zarith. case (spec_ww_to_Z x); auto with zarith. unfold base. apply Zdiv_lt_upper_bound. auto with zarith. rewrite <- Zpower_exp by auto with zarith. apply Z.lt_le_trans with (base (ww_digits (ZnZ.digits w_op))). case (spec_ww_to_Z x); auto with zarith. unfold base; apply Zpower_le_monotone. auto with zarith. split. auto with zarith. assert (0 < Zpos p); auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux