Don't pose any disjunctions in div_mod_to_quot_rem

Disjunctions seem to have a negative performance impact, so let's try
implications instead.

1 files changed, 9 insertions, 9 deletions

diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 387f258bdd..1e0922e1ca 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -19,17 +19,17 @@ Local Open Scope Z_scope.
     information. *)
 
 Module Z.
-  Lemma div_mod_cases x y
-  : ((x = y * (x/y) + x mod y /\ (0 <= x mod y < y \/ y < x mod y <= 0))
-     \/ (y = 0 /\ x / y = 0 /\ x mod y = 0)).
-  Proof.
-    destruct (Z.eq_dec y 0); subst;
-      [ right | left; auto using Z.div_mod, Z.mod_bound_or ].
-    destruct x; cbv; repeat esplit.
-  Qed.
+  Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0.
+  Proof. intro; subst; destruct x; reflexivity. Qed.
+  Lemma div_0_r_ext x y : y = 0 -> x / y = 0.
+  Proof. intro; subst; destruct x; reflexivity. Qed.
 
   Ltac div_mod_to_quot_rem_generalize x y :=
-    pose proof (div_mod_cases x y);
+    pose proof (Z.div_mod x y);
+    pose proof (Z.mod_pos_bound x y);
+    pose proof (Z.mod_neg_bound x y);
+    pose proof (div_0_r_ext x y);
+    pose proof (mod_0_r_ext x y);
     let q := fresh "q" in
     let r := fresh "r" in
     set (q := x / y) in *;