proposition: Theorem spec_ww_div21 : forall a1 a2 b, wwB/2 <= [[b]] -> [[a1]] < [[b]] -> let (q,r) := ww_div21 a1 a2 b in [[a1]] *wwB+[[a2]] = [[q]] * [[b]] + [[r]] /\ 0 <= [[r]] < [[b]].
proof: Proof. assert (U:= lt_0_wB w_digits). assert (U1:= lt_0_wwB w_digits). intros a1 a2 b H Hlt; unfold ww_div21. Spec_ww_to_Z b; assert (Eq: 0 < [[b]]). Spec_ww_to_Z a1;lia. generalize Hlt H ;clear Hlt H;case a1. intros H1 H2;simpl in H1;Spec_ww_to_Z a2. rewrite spec_ww_compare. case Z.compare_spec; simpl;try rewrite spec_ww_1;autorewrite with rm10; intros. 1-2: zarith. rewrite spec_ww_sub;simpl. rewrite Zmod_small by zarith. split. ring. enough (wwB <= 2*[[b]]) by zarith. rewrite wwB_div;zarith. intros a1h a1l. Spec_w_to_Z a1h;Spec_w_to_Z a1l. Spec_ww_to_Z a2. destruct a2 as [ |a3 a4]; (destruct b as [ |b1 b2];[unfold Z.le in Eq;discriminate Eq|idtac]); try (Spec_w_to_Z a3; Spec_w_to_Z a4); Spec_w_to_Z b1; Spec_w_to_Z b2; intros Hlt H; match goal with |-context [w_div32 ?X ?Y ?Z ?T ?U] => generalize (@spec_w_div32 X Y Z T U); case (w_div32 X Y Z T U); intros q1 r H0 end; (assert (Eq1: wB / 2 <= [|b1|]);[ apply (@beta_lex (wB / 2) 0 [|b1|] [|b2|] wB); [ | zarith | zarith ]; autorewrite with rm10;repeat rewrite (Z.mul_comm wB); rewrite <- wwB_div_2; trivial | generalize (H0 Eq1 Hlt);clear H0;destruct r as [ |r1 r2];simpl; try rewrite spec_w_0; try rewrite spec_w_0W;repeat rewrite Z.add_0_r; intros (H1,H2) ]). split;[rewrite wwB_wBwB; rewrite Z.pow_2_r | trivial]. rewrite Z.mul_assoc;rewrite Z.mul_add_distr_r;rewrite <- Z.mul_assoc; rewrite <- Z.pow_2_r; rewrite <- wwB_wBwB;rewrite H1;ring. destruct H2 as (H2,H3);match goal with |-context [w_div32 ?X ?Y ?Z ?T ?U] => generalize (@spec_w_div32 X Y Z T U); case (w_div32 X Y Z T U); intros q r H0;generalize (H0 Eq1 H3);clear H0;intros (H4,H5) end. split;[rewrite wwB_wBwB | trivial]. rewrite Z.pow_2_r. rewrite Z.mul_assoc;rewrite Z.mul_add_distr_r;rewrite <- Z.mul_assoc; rewrite <- Z.pow_2_r. rewrite <- wwB_wBwB;rewrite H1. rewrite spec_w_0 in H4;rewrite Z.add_0_r in H4. repeat rewrite Z.mul_add_distr_r. rewrite <- (Z.mul_assoc [|r1|]). rewrite <- Z.pow_2_r; rewrite <- wwB_wBwB;rewrite H4;simpl;ring. split;[rewrite wwB_wBwB | split; [ zarith | ] ]. replace (([|a1h|] * wB + [|a1l|]) * wB^2 + ([|a3|] * wB + [|a4|])) with (([|a1h|] * wwB + [|a1l|] * wB + [|a3|])*wB+ [|a4|]). rewrite H1;ring. rewrite wwB_wBwB;ring. change [|a4|] with (0*wB+[|a4|]);apply beta_lex_inv. 2-3: zarith. enough (1 <= wB/2) by zarith. assert (H_:= wB_pos w_digits);apply Zdiv_le_lower_bound;zarith. destruct H2 as (H2,H3);match goal with |-context [w_div32 ?X ?Y ?Z ?T ?U] => generalize (@spec_w_div32 X Y Z T U); case (w_div32 X Y Z T U); intros q r H0;generalize (H0 Eq1 H3);clear H0;intros (H4,H5) end. split;trivial. replace (([|a1h|] * wB + [|a1l|]) * wwB + ([|a3|] * wB + [|a4|])) with (([|a1h|] * wwB + [|a1l|] * wB + [|a3|])*wB + [|a4|]); [rewrite H1 | rewrite wwB_wBwB;ring]. replace (([|q1|]*([|b1|]*wB+[|b2|])+([|r1|]*wB+[|r2|]))*wB+[|a4|]) with (([|q1|]*([|b1|]*wB+[|b2|]))*wB+([|r1|]*wwB+[|r2|]*wB+[|a4|])); [rewrite H4;simpl|rewrite wwB_wBwB];ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub