Reorder arguments of comparison predicates as they should

mathcomp/algebra/poly.v

@@ -304,7 +304,7 @@ Canonical opp_poly_unlockable := [unlockable fun opp_poly].
 
 Fact coef_add_poly p q i : (add_poly p q)`_i = p`_i + q`_i.
 Proof.
-rewrite unlock coef_poly; case: (ltnP i) => //.
+rewrite unlock coef_poly; case: leqP => //.
 by rewrite geq_max => /andP[le_p_i le_q_i]; rewrite !nth_default ?add0r.
 Qed.
 

mathcomp/algebra/ssrnum.v

@@ -3771,25 +3771,21 @@ Lemma oppr_min : {morph -%R : x y / min x y >-> max x y : R}.
 Proof. by move=> x y; rewrite -[max _ _]opprK oppr_max !opprK. Qed.
 
 Lemma addr_minl : @left_distributive R R +%R min.
-Proof.
-by move=> x y z; case: leP; case: leP => //; rewrite lter_add2; case: leP.
-Qed.
+Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed.
 
 Lemma addr_minr : @right_distributive R R +%R min.
 Proof. by move=> x y z; rewrite !(addrC x) addr_minl. Qed.
 
 Lemma addr_maxl : @left_distributive R R +%R max.
-Proof.
-by move=> x y z; case: leP; case: leP => //; rewrite lter_add2; case: leP.
-Qed.
+Proof. by move=> x y z; case: (leP (_ + _)); rewrite lter_add2; case: leP. Qed.
 
 Lemma addr_maxr : @right_distributive R R +%R max.
 Proof. by move=> x y z; rewrite !(addrC x) addr_maxl. Qed.
 
 Lemma minr_pmulr x y z : 0 <= x -> x * min y z = min (x * y) (x * z).
 Proof.
 case: sgrP=> // hx _; first by rewrite hx !mul0r meetxx.
-by case: leP; case: leP => //; rewrite lter_pmul2l //; case: leP.
+by case: (leP (_ * _)); rewrite lter_pmul2l //; case: leP.
 Qed.
 
 Lemma minr_nmulr x y z : x <= 0 -> x * min y z = max (x * y) (x * z).

mathcomp/ssreflect/fintype.v

@@ -2037,7 +2037,7 @@ Proof.
 (* match representation is changed to omit these then this proof could reduce *)
 (* to by rewrite /split; case: ltnP; [left | right. rewrite subnKC].          *)
 set lt_i_m := i < m; rewrite /split.
-by case: {-}_ lt_i_m _ _ _ _ / ltnP; [left | right; rewrite subnKC].
+by case: _ _ _ _ {-}_ lt_i_m / ltnP; [left | right; rewrite subnKC].
 Qed.
 
 Definition unsplit {m n} (jk : 'I_m + 'I_n) :=

mathcomp/ssreflect/order.v

@@ -1186,35 +1186,35 @@ Context {T : distrLatticeType}.
 Definition meet : T -> T -> T := DistrLattice.meet (DistrLattice.class T).
 Definition join : T -> T -> T := DistrLattice.join (DistrLattice.class T).
 
-Variant lel_xor_gt (x y : T) : bool -> bool -> T -> T -> T -> T -> Set :=
-  | LelNotGt of x <= y : lel_xor_gt x y true false x x y y
-  | GtlNotLe of y < x  : lel_xor_gt x y false true y y x x.
+Variant lel_xor_gt (x y : T) : T -> T -> T -> T -> bool -> bool -> Set :=
+  | LelNotGt of x <= y : lel_xor_gt x y x x y y true false
+  | GtlNotLe of y < x  : lel_xor_gt x y y y x x false true.
 
-Variant ltl_xor_ge (x y : T) : bool -> bool -> T -> T -> T -> T -> Set :=
-  | LtlNotGe of x < y  : ltl_xor_ge x y false true x x y y
-  | GelNotLt of y <= x : ltl_xor_ge x y true false y y x x.
+Variant ltl_xor_ge (x y : T) : T -> T -> T -> T -> bool -> bool -> Set :=
+  | LtlNotGe of x < y  : ltl_xor_ge x y x x y y false true
+  | GelNotLt of y <= x : ltl_xor_ge x y y y x x true false.
 
 Variant comparel (x y : T) :
-  bool -> bool -> bool -> bool -> bool -> bool -> T -> T -> T -> T -> Set :=
+  T -> T -> T -> T -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | ComparelLt of x < y : comparel x y
-    false false false true false true x x y y
+    x x y y false false false true false true
   | ComparelGt of y < x : comparel x y
-    false false true false true false y y x x
+    y y x x false false true false true false
   | ComparelEq of x = y : comparel x y
-    true true true true false false x x x x.
+    x x x x true true true true false false.
 
 Variant incomparel (x y : T) :
-  bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool ->
-  T -> T -> T -> T -> Set :=
+  T -> T -> T -> T ->
+  bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | InComparelLt of x < y : incomparel x y
-    false false false true false true true true x x y y
+    x x y y false false false true false true true true
   | InComparelGt of y < x : incomparel x y
-    false false true false true false true true y y x x
+    y y x x false false true false true false true true
   | InComparel of x >< y  : incomparel x y
-    false false false false false false false false
     (meet x y) (meet x y) (join x y) (join x y)
+    false false false false false false false false
   | InComparelEq of x = y : incomparel x y
-    true true true true false false true true x x x x.
+    x x x x true true true true false false true true.
 
 End DistrLatticeDef.
 
@@ -2828,8 +2828,8 @@ Lemma joinIr : right_distributive (@join _ L) (@meet _ L).
 Proof. exact: (@meetUr _ [distrLatticeType of L^c]). Qed.
 
 Lemma lcomparableP x y : incomparel x y
-  (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
-  (y >=< x) (x >=< y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+  (y `&` x) (x `&` y) (y `|` x) (x `|` y)
+  (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y) (y >=< x) (x >=< y).
 Proof.
 by case: (comparableP x) => [hxy|hxy|hxy|->]; do 1?have hxy' := ltW hxy;
   rewrite ?(meetxx, joinxx, meetC y, joinC y)
@@ -2838,16 +2838,16 @@ by case: (comparableP x) => [hxy|hxy|hxy|->]; do 1?have hxy' := ltW hxy;
 Qed.
 
 Lemma lcomparable_ltgtP x y : x >=< y ->
-  comparel x y (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y)
-           (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+  comparel x y (y `&` x) (x `&` y) (y `|` x) (x `|` y)
+               (y == x) (x == y) (x >= y) (x <= y) (x > y) (x < y).
 Proof. by case: (lcomparableP x) => // *; constructor. Qed.
 
 Lemma lcomparable_leP x y : x >=< y ->
-  lel_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+  lel_xor_gt x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x).
 Proof. by move/lcomparable_ltgtP => [/ltW xy|xy|->]; constructor. Qed.
 
 Lemma lcomparable_ltP x y : x >=< y ->
-  ltl_xor_ge x y (y <= x) (x < y) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+  ltl_xor_ge x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (y <= x) (x < y).
 Proof. by move=> /lcomparable_ltgtP [xy|/ltW xy|->]; constructor. Qed.
 
 End DistrLatticeTheoryJoin.
@@ -3835,7 +3835,7 @@ Let T_total_distrLatticeType : distrLatticeType tt :=
 Implicit Types (x y z : T_total_distrLatticeType).
 
 Fact leP x y :
-  lel_xor_gt x y (x <= y) (y < x) (y `&` x) (x `&` y) (y `|` x) (x `|` y).
+  lel_xor_gt x y (y `&` x) (x `&` y) (y `|` x) (x `|` y) (x <= y) (y < x).
 Proof. by apply/lcomparable_leP/le_total. Qed.
 Fact meetE x y : meet m x y = x `&` y.
 Proof. by rewrite meet_def (_ : lt m x y = (x < y)) //; case: (leP y). Qed.

mathcomp/ssreflect/ssrnat.v

@@ -778,23 +778,23 @@ Proof. by move=> m n1 n2; rewrite !(minnC m) minn_maxl. Qed.
 
 (* Comparison predicates. *)
 
-Variant leq_xor_gtn m n : bool -> bool -> nat -> nat -> nat -> nat -> Set :=
-  | LeqNotGtn of m <= n : leq_xor_gtn m n true false m m n n
-  | GtnNotLeq of n < m  : leq_xor_gtn m n false true n n m m.
+Variant leq_xor_gtn m n : nat -> nat -> nat -> nat -> bool -> bool -> Set :=
+  | LeqNotGtn of m <= n : leq_xor_gtn m n m m n n true false
+  | GtnNotLeq of n < m  : leq_xor_gtn m n n n m m false true.
 
-Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m)
-                             (minn n m) (minn m n) (maxn n m) (maxn m n).
+Lemma leqP m n : leq_xor_gtn m n (minn n m) (minn m n) (maxn n m) (maxn m n)
+                                 (m <= n) (n < m).
 Proof.
 rewrite (minnC m) /minn (maxnC m) /maxn ltnNge.
 by case le_mn: (m <= n); constructor; rewrite //= ltnNge le_mn.
 Qed.
 
-Variant ltn_xor_geq m n : bool -> bool -> nat -> nat -> nat -> nat -> Set :=
-  | LtnNotGeq of m < n  : ltn_xor_geq m n false true m m n n
-  | GeqNotLtn of n <= m : ltn_xor_geq m n true false n n m m.
+Variant ltn_xor_geq m n : nat -> nat -> nat -> nat -> bool -> bool -> Set :=
+  | LtnNotGeq of m < n  : ltn_xor_geq m n m m n n false true
+  | GeqNotLtn of n <= m : ltn_xor_geq m n n n m m true false.
 
-Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n)
-                             (minn n m) (minn m n) (maxn n m) (maxn m n).
+Lemma ltnP m n : ltn_xor_geq m n (minn n m) (minn m n) (maxn n m) (maxn m n)
+                                 (n <= m) (m < n).
 Proof. by case: leqP; constructor. Qed.
 
 Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
@@ -804,18 +804,18 @@ Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
 Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n).
 Proof. by case: n; constructor. Qed.
 
-Variant compare_nat m n : bool -> bool -> bool -> bool -> bool -> bool ->
-                          nat -> nat -> nat -> nat -> Set :=
+Variant compare_nat m n : nat -> nat -> nat -> nat ->
+                          bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | CompareNatLt of m < n :
-      compare_nat m n false false false true false true m m n n
+      compare_nat m n m m n n false false false true false true
   | CompareNatGt of m > n :
-      compare_nat m n false false true false true false n n m m
+      compare_nat m n n n m m false false true false true false
   | CompareNatEq of m = n :
-      compare_nat m n true true true true false false m m m m.
+      compare_nat m n m m m m true true true true false false.
 
 Lemma ltngtP m n :
-  compare_nat m n (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n)
-              (minn n m) (minn m n) (maxn n m) (maxn m n).
+  compare_nat m n (minn n m) (minn m n) (maxn n m) (maxn m n)
+                  (n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n).
 Proof.
 rewrite !ltn_neqAle [_ == n]eq_sym; have [mn|] := ltnP m n.
   by rewrite ltnW // gtn_eqF //; constructor.