Bad instance selection for default_cut_minus

I was working on a development that used cut_minus with Z and ran into a situation where cut_minus was returning negative integers. I was able to create a small case demonstrating the issue and narrowed it down to peculiar typeclass resolution. It is selecting the decision instance in default_cut_minus before the Le and coming up with the decision for equiv on Z leading equiv to be used for le within default_cut_minus. I'm not anywhere near enough of a typeclasses wizard to know what if anything can be done to force the intended instances to be selected.

The input below demonstrates the issue on coq 8.19.1 and rocq 9.0.1 with math-classes master.

From MathClasses Require Import
  interfaces.canonical_names
  interfaces.additional_operations
  implementations.stdlib_binary_integers
  orders.integers
  theory.cut_minus
.

From Coq Require Import BinIntDef.

(* cut_minus 1 2 is supposed to evaluate to 0, but it results in -1 *)
Compute (cut_minus 1%Z 2%Z).

Type (@equiv Z _ : Le Z).

(* Typeclass debug logs show that instance resolution is done for
   Decision before it is done for Le and the first instance found
   is the instance for deciding equiv. As we can see above, equiv
   is typeable as an Le instance so this solution is accepted. Thus,
   the cut_minus above is equivalent to the following. *)
Compute (default_cut_minus (R:=Z) (o:=Z_equiv) 1%Z 2%Z).

Example cm_selected_instance : cut_minus (A:=Z) ≡ default_cut_minus (R:=Z) (o:=Z_equiv) := eq_refl.

(* cut_minus 1 2 is supposed to evaluate to 0 *)
Example bad_cut_minus : (cut_minus 1%Z 2%Z ≡ 0) := eq_refl.

Start with theory.cut_minus and the related interfaces and implementations modules named in the report, then run the provided Rocq reproduction on the reported versions. Trace the typeclass resolution for default_cut_minus and confirm that cut_minus 1 2 computes to 0 using the intended Le instance; the issue is done when the bad decision-instance selection no longer occurs.