Add a compatibility layer and a changelog entry

CHANGELOG_UNRELEASED.md

@@ -92,6 +92,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
     `Num` module. However, instances of the number structures may require
     changes.
 
+- Extended comparison predicates `leqP`, `ltnP`, and `ltngtP` in ssrnat to
+  allow case analysis on `minn` and `maxn`.
+  + The compatibility layer for the version 1.10 is provided as the
+    `ssrnat.mc_1_10` module. One may compile proofs compatible with the version
+    1.10 in newer versions by using this module.
+
 ### Renamed
 
 - `real_lerP` -> `real_leP`

mathcomp/ssreflect/ssrnat.v

@@ -1883,3 +1883,38 @@ Lemma ltngtP m n : compare_nat m n (m <= n) (n <= m) (m < n)
 Proof. by case: ltngtP; constructor. Qed.
 
 End mc_1_9.
+
+Module mc_1_10.
+
+Variant leq_xor_gtn m n : bool -> bool -> Set :=
+  | LeqNotGtn of m <= n : leq_xor_gtn m n true false
+  | GtnNotLeq of n < m  : leq_xor_gtn m n false true.
+
+Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m).
+Proof. by case: leqP; constructor. Qed.
+
+Variant ltn_xor_geq m n : bool -> bool -> Set :=
+  | LtnNotGeq of m < n  : ltn_xor_geq m n false true
+  | GeqNotLtn of n <= m : ltn_xor_geq m n true false.
+
+Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n).
+Proof. by case: ltnP; constructor. Qed.
+
+Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
+  | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false
+  | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true.
+
+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 -> Set :=
+  | CompareNatLt of m < n : compare_nat m n false false false true false true
+  | CompareNatGt of m > n : compare_nat m n false false true false true false
+  | CompareNatEq of m = n : compare_nat m n 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).
+Proof. by case: ltngtP; constructor. Qed.
+
+End mc_1_10.