Add a non-overflow precondition to diveucl_21 to align it on standard implementations.

1 files changed, 3 insertions, 20 deletions

diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index c81ba02230..9e9481341f 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -388,7 +388,7 @@ Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y.
 Axiom diveucl_21_spec :  forall a1 a2 b,
    let (q,r) := diveucl_21 a1 a2 b in
    let (q',r') := Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|] in
-   [|q|] = Z.modulo q' wB /\ [|r|] = r'.
+   [|a1|] < [|b|] -> [|q|] = q' /\ [|r|] = r'.
 
 Axiom addmuldiv_def_spec : forall p x y,
   addmuldiv p x y = addmuldiv_def p x y.
@@ -1421,26 +1421,9 @@ Proof.
  generalize (Z_div_mod ([|a1|]*wB+[|a2|]) [|b|] H).
  revert W.
  destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl ([|a1|]*wB+[|a2|]) [|b|]).
- intros (H', H''); rewrite H', H''; clear H' H''.
+ intros (H', H''); auto; rewrite H', H''; clear H' H''.
  intros (H', H''); split; [ |exact H''].
- rewrite H', Zmult_comm, Z.mod_small; [reflexivity| ].
- split.
- { revert H'; case z; [now simpl..|intros p H'].
-   exfalso; apply (Z.lt_irrefl 0), (Z.le_lt_trans _ ([|a1|] * wB + [|a2|])).
-   { now apply Z.add_nonneg_nonneg; [apply Z.mul_nonneg_nonneg| ]. }
-   rewrite H'; apply (Zplus_lt_reg_r _ _ (- z0)); ring_simplify.
-   apply (Z.le_lt_trans _ (- [|b|])); [ |now auto with zarith].
-   rewrite Z.opp_eq_mul_m1; apply Zmult_le_compat_l; [ |now apply Wb].
-   rewrite <-!Pos2Z.opp_pos, <-Z.opp_le_mono.
-   now change 1 with (Z.succ 0); apply Zlt_le_succ. }
- rewrite <-Z.nle_gt; intro Hz; revert H2; apply Zle_not_lt.
- rewrite (Z.div_unique_pos (wB * [|a1|] + [|a2|]) wB [|a1|] [|a2|]);
-   [ |now simpl..].
- rewrite Z.mul_comm, H'.
- rewrite (Z.div_unique_pos (wB * [|b|] + z0) wB [|b|] z0) at 1;
-   [ |split; [ |apply (Z.lt_trans _ [|b|])]; now simpl|reflexivity].
- apply Z_div_le; [now simpl| ]; rewrite Z.mul_comm; apply Zplus_le_compat_r.
- now apply Zmult_le_compat_l.
+ now rewrite H', Zmult_comm.
 Qed.
 
 Lemma div2_phi ih il j: (2^62 <= [|j|] -> [|ih|] < [|j|] ->