numbers.v: Don't Qed Decision instances

Noticed from a compute_done failure.

Also, use abstract to still hide proof-irrelevant terms from computation.

stdpp/numbers.v

@@ -165,7 +165,8 @@ Module Nat.
 
   Global Instance divide_dec : RelDecision Nat.divide.
   Proof.
-    refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
+    refine (λ x y, cast_if (decide (lcm x y = y)));
+      abstract (by rewrite Nat.divide_lcm_iff).
   Defined.
   Global Instance divide_po : PartialOrder divide.
   Proof.
@@ -1018,7 +1019,7 @@ Module Qp.
   Global Instance eq_dec : EqDecision Qp.
   Proof.
     refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
-      by rewrite <-to_Qc_inj_iff.
+      abstract (by rewrite <-to_Qc_inj_iff).
   Defined.
 
   Definition add (p q : Qp) : Qp :=
@@ -1063,13 +1064,13 @@ Module Qp.
   Global Instance le_dec : RelDecision le.
   Proof.
     refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc));
-      by rewrite to_Qc_inj_le.
-  Qed.
+      abstract (by rewrite to_Qc_inj_le).
+  Defined.
   Global Instance lt_dec : RelDecision lt.
   Proof.
     refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc));
-      by rewrite to_Qc_inj_lt.
-  Qed.
+      abstract (by rewrite to_Qc_inj_lt).
+  Defined.
   Global Instance lt_pi p q : ProofIrrel (lt p q).
   Proof. destruct p, q; apply _. Qed.