proposition: Theorem spec_w_div21c : forall a1 a2 b, wB/2 <= [|b|] -> let (q,r) := w_div21c a1 a2 b in [|a1|] * wB + [|a2|] = [+|q|] * [|b|] + [|r|] /\ 0 <= [|r|] < [|b|].
proof: Proof. intros a1 a2 b Hb; unfold w_div21c. assert (H: 0 < [|b|]). { assert (U := wB_pos w_digits). apply Z.lt_le_trans with (2 := Hb). apply Z.lt_le_trans with 1. zarith. apply Zdiv_le_lower_bound; zarith. } rewrite !spec_w_compare. repeat case Z.compare_spec. intros H1 H2; split. unfold interp_carry; autorewrite with w_rewrite rm10. rewrite H1; rewrite H2; ring. autorewrite with w_rewrite; zarith. intros H1 H2; split. unfold interp_carry; autorewrite with w_rewrite rm10. rewrite H2; ring. destruct (spec_to_Z a2);zarith. intros H1 H2; split. unfold interp_carry; autorewrite with w_rewrite rm10. rewrite H2; rewrite Zmod_small. ring. destruct (spec_to_Z a2);zarith. rewrite spec_w_sub by zarith. destruct (spec_to_Z a2) as [H3 H4]. rewrite Zmod_small by zarith. split. zarith. enough ([|a2|] < 2 * [|b|]) by zarith. apply Z.lt_le_trans with (2 * (wB / 2)). 2: zarith. rewrite wB_div_2; auto. intros H1. match goal with |- context[w_div21 ?y ?z ?t] => generalize (@spec_w_div21 y z t Hb H1); case (w_div21 y z t); simpl; autorewrite with w_rewrite; auto end. intros H1. assert (H2: [|w_sub a1 b|] < [|b|]). rewrite spec_w_sub by zarith. rewrite Zmod_small. enough ([|a1|] < 2 * [|b|]) by zarith. apply Z.lt_le_trans with (2 * (wB / 2)). 2: zarith. rewrite wB_div_2; auto. destruct (spec_to_Z a1);zarith. destruct (spec_to_Z a1);zarith. match goal with |- context[w_div21 ?y ?z ?t] => generalize (@spec_w_div21 y z t Hb H2); case (w_div21 y z t); autorewrite with w_rewrite; auto end. intros w0 w1; replace [+|C1 w0|] with (wB + [|w0|]). rewrite Zmod_small. intros (H3, H4); split; auto. rewrite Z.mul_add_distr_r. rewrite <- Z.add_assoc; rewrite <- H3; ring. split. zarith. assert ([|a1|] < 2 * [|b|]). apply Z.lt_le_trans with (2 * (wB / 2)). 2: zarith. rewrite wB_div_2; auto. destruct (spec_to_Z a1);zarith. destruct (spec_to_Z a1);zarith. simpl; case wB; auto. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase