Merge pull request #429 from pi8027/extend-nat-comparison

Extend comparison predicates for nat with minn and maxn and reorder arguments of those in order.v

6 files changed, 141 insertions, 107 deletions

diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 06a6ff1..b366055 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -120,7 +120,7 @@ Proof. by case: d => // d; rewrite -[n in n %/ _]muln1 mulKn. Qed.
 
 Lemma divnMl p m d : p > 0 -> p * m %/ (p * d) = m %/ d.
 Proof.
-move=> p_gt0; case: (posnP d) => [-> | d_gt0]; first by rewrite muln0.
+move=> p_gt0; have [->|d_gt0] := posnP d; first by rewrite muln0.
 rewrite [RHS]/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd.
 rewrite mulnDr mulnCA divnMDl; last by rewrite muln_gt0 p_gt0.
 by rewrite addnC divn_small // ltn_pmul2l.
@@ -544,9 +544,9 @@ Lemma edivnS m d : 0 < d -> edivn m.+1 d =
 Proof.
 case: d => [|[|d]] //= _; first by rewrite edivn_def modn1 dvd1n !divn1.
 rewrite -addn1 /dvdn modn_def edivnD//= (@modn_small 1)// (@divn_small 1)//.
-rewrite addn1 addn0 ltnS; case: (ltngtP _ d.+1) => [ | |->].
-- by rewrite addn0 mul0n subn0.
+rewrite addn1 addn0 ltnS; have [||<-] := ltngtP d.+1.
 - by rewrite ltnNge -ltnS ltn_pmod.
+- by rewrite addn0 mul0n subn0.
 - by rewrite addn1 mul1n subnn.
 Qed.
 
@@ -656,10 +656,7 @@ Lemma gcdn_idPr {m n} : reflect (gcdn m n = n) (n %| m).
 Proof. by rewrite gcdnC; apply: gcdn_idPl. Qed.
 
 Lemma expn_min e m n : e ^ minn m n = gcdn (e ^ m) (e ^ n).
-Proof.
-rewrite /minn; case: leqP; [rewrite gcdnC | move/ltnW];
-  by move/(dvdn_exp2l e)/gcdn_idPl.
-Qed.
+Proof. by case: leqP => [|/ltnW] /(dvdn_exp2l e) /gcdn_idPl; rewrite gcdnC. Qed.
 
 Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n.
 Proof. by rewrite [in RHS](divn_eq n m) gcdnMDl. Qed.
@@ -863,10 +860,7 @@ Lemma lcmn_idPl {m n} : reflect (lcmn m n = m) (n %| m).
 Proof. by rewrite lcmnC; apply: lcmn_idPr. Qed.
 
 Lemma expn_max e m n : e ^ maxn m n = lcmn (e ^ m) (e ^ n).
-Proof.
-rewrite /maxn; case: leqP; [rewrite lcmnC | move/ltnW];
- by move/(dvdn_exp2l e)/lcmn_idPr.
-Qed.
+Proof. by case: leqP => [|/ltnW] /(dvdn_exp2l e) /lcmn_idPl; rewrite lcmnC. Qed.
 
 (* Coprime factors *)
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 14d623f..6c27b73 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/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) :=
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 5c8f251..8f3efaf 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -1216,35 +1216,35 @@ Context {T : latticeType}.
 Definition meet : T -> T -> T := Lattice.meet (Lattice.class T).
 Definition join : T -> T -> T := Lattice.join (Lattice.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 LatticeDef.
 
@@ -3218,8 +3218,8 @@ Lemma leU2 x y z t : x <= z -> y <= t -> x `|` y <= z `|` t.
 Proof. exact: (@leI2 _ [latticeType of L^d]). 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)
@@ -3228,16 +3228,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 LatticeTheoryJoin.
@@ -4556,10 +4556,10 @@ Module NatOrder.
 Section NatOrder.
 
 Lemma minnE x y : minn x y = if (x <= y)%N then x else y.
-Proof. by case: leqP => [/minn_idPl|/ltnW /minn_idPr]. Qed.
+Proof. by case: leqP. Qed.
 
 Lemma maxnE x y : maxn x y = if (y <= x)%N then x else y.
-Proof. by case: leqP => [/maxn_idPl|/ltnW/maxn_idPr]. Qed.
+Proof. by case: leqP. Qed.
 
 Lemma ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N.
 Proof. by rewrite ltn_neqAle eq_sym. Qed.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index d8f5939..b71f5e7 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -583,7 +583,7 @@ move=> m_gt0 n_gt0; apply/eqP/hasPn=> [mn1 p | no_p_mn].
   rewrite /= !mem_primes m_gt0 n_gt0 /= => /andP[pr_p p_n].
   have:= prime_gt1 pr_p; rewrite pr_p ltnNge -mn1 /=; apply: contra => p_m.
   by rewrite dvdn_leq ?gcdn_gt0 ?m_gt0 // dvdn_gcd ?p_m.
-case: (ltngtP (gcdn m n) 1) => //; first by rewrite ltnNge gcdn_gt0 ?m_gt0.
+apply/eqP; rewrite eqn_leq gcdn_gt0 m_gt0 andbT leqNgt; apply/negP.
 move/pdiv_prime; set p := pdiv _ => pr_p.
 move/implyP: (no_p_mn p); rewrite /= !mem_primes m_gt0 n_gt0 pr_p /=.
 by rewrite !(dvdn_trans (pdiv_dvd _)) // (dvdn_gcdl, dvdn_gcdr).
@@ -956,8 +956,7 @@ Proof. by rewrite ltn_neqAle part_gt0 andbT eq_sym p_part_eq1 negbK. Qed.
 
 Lemma primes_part pi n : primes n`_pi = filter (mem pi) (primes n).
 Proof.
-have ltnT := ltn_trans.
-case: (posnP n) => [-> | n_gt0]; first by rewrite partn0.
+have ltnT := ltn_trans; have [->|n_gt0] := posnP n; first by rewrite partn0.
 apply: (eq_sorted_irr ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //.
 move=> p; rewrite mem_filter /= !mem_primes n_gt0 part_gt0 /=.
 apply/andP/and3P=> [[p_pr] | [pi_p p_pr dv_p_n]].
@@ -1194,15 +1193,14 @@ Lemma part_pnat_id pi n : pi.-nat n -> n`_pi = n.
 Proof.
 case/andP=> n_gt0 pi_n.
 rewrite -{2}(partnT n_gt0) /partn big_mkcond; apply: eq_bigr=> p _.
-case: (posnP (logn p n)) => [-> |]; first by rewrite if_same.
+have [->|] := posnP (logn p n); first by rewrite if_same.
 by rewrite logn_gt0 => /(allP pi_n)/= ->.
 Qed.
 
 Lemma part_p'nat pi n : pi^'.-nat n -> n`_pi = 1.
 Proof.
 case/andP=> n_gt0 pi'_n; apply: big1_seq => p /andP[pi_p _].
-case: (posnP (logn p n)) => [-> //|].
-by rewrite logn_gt0; move/(allP pi'_n); case/negP.
+by have [-> //|] := posnP (logn p n); rewrite logn_gt0; case/(allP pi'_n)/negP.
 Qed.
 
 Lemma partn_eq1 pi n : n > 0 -> (n`_pi == 1) = pi^'.-nat n.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index f73c119..ed7c1dd 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -890,9 +890,7 @@ Lemma all_rev a s : all a (rev s) = all a s.
 Proof. by rewrite !all_count count_rev size_rev. Qed.
 
 Lemma rev_nseq n x : rev (nseq n x) = nseq n x.
-Proof.
-by elim: n => [// | n IHn]; rewrite -{1}(addn1 n) nseq_addn rev_cat IHn.
-Qed.
+Proof. by elim: n => // n IHn; rewrite -{1}(addn1 n) nseq_addn rev_cat IHn. Qed.
 
 End Sequences.
 
@@ -1759,14 +1757,14 @@ Proof. exact (can_inj rotrK). Qed.
 Lemma take_rev s : take n0 (rev s) = rev (drop (size s - n0) s).
 Proof.
 set m := _ - n0; rewrite -[s in LHS](cat_take_drop m) rev_cat take_cat.
-rewrite size_rev size_drop -minnE minnC ltnNge geq_minl [in take m s]/m /minn.
+rewrite size_rev size_drop -minnE minnC leq_min ltnn /m.
 by have [_|/eqnP->] := ltnP; rewrite ?subnn take0 cats0.
 Qed.
 
 Lemma drop_rev s : drop n0 (rev s) = rev (take (size s - n0) s).
 Proof.
 set m := _ - n0; rewrite -[s in LHS](cat_take_drop m) rev_cat drop_cat.
-rewrite size_rev size_drop -minnE minnC ltnNge geq_minl /= /m /minn.
+rewrite size_rev size_drop -minnE minnC leq_min ltnn /m.
 by have [_|/eqnP->] := ltnP; rewrite ?take0 // subnn drop0.
 Qed.
 
@@ -2434,11 +2432,10 @@ Proof.
 by move/subnKC <-; rewrite addSnnS iota_add nth_cat size_iota ltnn subnn.
 Qed.
 
-Lemma mem_iota m n i : (i \in iota m n) = (m <= i) && (i < m + n).
+Lemma mem_iota m n i : (i \in iota m n) = (m <= i < m + n).
 Proof.
 elim: n m => [|n IHn] /= m; first by rewrite addn0 ltnNge andbN.
-rewrite -addSnnS leq_eqVlt in_cons eq_sym.
-by case: eqP => [->|_]; [rewrite leq_addr | apply: IHn].
+by rewrite in_cons IHn addnS ltnS; case: ltngtP => // ->; rewrite leq_addr.
 Qed.
 
 Lemma iota_uniq m n : uniq (iota m n).
@@ -2446,17 +2443,16 @@ Proof. by elim: n m => //= n IHn m; rewrite mem_iota ltnn /=. Qed.
 
 Lemma take_iota k m n : take k (iota m n) = iota m (minn k n).
 Proof.
-rewrite /minn; case: ltnP => [lt_k_n|le_n_k].
-  by elim: k n lt_k_n m => [|k IHk] [|n]//= H m; rewrite IHk.
+have [lt_k_n|le_n_k] := ltnP.
+  by elim: k n lt_k_n m => [|k IHk] [|n] //= H m; rewrite IHk.
 by apply: take_oversize; rewrite size_iota.
 Qed.
 
 Lemma drop_iota k m n : drop k (iota m n) = iota (m + k) (n - k).
 Proof.
-by elim: k m n => [|k IHk] m [|n]//=; rewrite ?addn0// IHk addSn addnS subSS.
+by elim: k m n => [|k IHk] m [|n] //=; rewrite ?addn0 // IHk addnS subSS.
 Qed.
 
-
 (* Making a sequence of a specific length, using indexes to compute items. *)
 
 Section MakeSeq.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index bccb968..7de4ad4 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -474,47 +474,6 @@ Arguments ltP {m n}.
 Lemma lt_irrelevance m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat.
 Proof. exact: (@le_irrelevance m.+1). Qed.
 
-(* Comparison predicates. *)
-
-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 rewrite ltnNge; case le_mn: (m <= n); constructor; rewrite // ltnNge le_mn.
-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: leqP; 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.
-rewrite !ltn_neqAle [_ == n]eq_sym; case: ltnP => [nm|].
-  by rewrite ltnW // gtn_eqF //; constructor.
-rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_mn eq_nm.
-  by rewrite ltn_eqF //; constructor.
-by rewrite eq_nm; constructor; apply/esym/eqP.
-Qed.
-
 (* Monotonicity lemmas *)
 
 Lemma leq_add2l p m n : (p + m <= p + n) = (m <= n).
@@ -656,13 +615,6 @@ Proof. by move=> np pm; rewrite !leq_subRL // addnC. Qed.
 Lemma ltn_subCl m n p : n <= m -> p <= m -> (m - n < p) = (m - p < n).
 Proof. by move=> nm pm; rewrite !ltn_subLR // addnC. Qed.
 
-(* Eliminating the idiom for structurally decreasing compare and subtract. *)
-Lemma subn_if_gt T m n F (E : T) :
-  (if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E).
-Proof.
-by case: leqP => [le_nm | /eqnP-> //]; rewrite -{1}(subnK le_nm) -addSn addnK.
-Qed.
-
 (* Max and min. *)
 
 Definition maxn m n := if m < n then n else m.
@@ -673,10 +625,13 @@ Lemma max0n : left_id 0 maxn.  Proof. by case. Qed.
 Lemma maxn0 : right_id 0 maxn. Proof. by []. Qed.
 
 Lemma maxnC : commutative maxn.
-Proof. by move=> m n; rewrite /maxn; case ltngtP. Qed.
+Proof. by rewrite /maxn; elim=> [|m ih] [] // n; rewrite !ltnS -!fun_if ih. Qed.
 
 Lemma maxnE m n : maxn m n = m + (n - m).
-Proof. by rewrite /maxn addnC; case: leqP => [/eqnP->|/ltnW/subnK]. Qed.
+Proof.
+rewrite /maxn; elim: m n => [|m ih] [|n]; rewrite ?addn0 //.
+by rewrite ltnS subSS addSn -ih; case: leq.
+Qed.
 
 Lemma maxnAC : right_commutative maxn.
 Proof. by move=> m n p; rewrite !maxnE -!addnA !subnDA -!maxnE maxnC. Qed.
@@ -727,10 +682,10 @@ Lemma min0n : left_zero 0 minn. Proof. by case. Qed.
 Lemma minn0 : right_zero 0 minn. Proof. by []. Qed.
 
 Lemma minnC : commutative minn.
-Proof. by move=> m n; rewrite /minn; case ltngtP. Qed.
+Proof. by rewrite /minn; elim=> [|m ih] [] // n; rewrite !ltnS -!fun_if ih. Qed.
 
 Lemma addn_min_max m n : minn m n + maxn m n = m + n.
-Proof. by rewrite /minn /maxn; case: ltngtP => // [_|->] //; apply: addnC. Qed.
+Proof. by rewrite /minn /maxn; case: (m < n) => //; exact: addnC. Qed.
 
 Lemma minnE m n : minn m n = m - (m - n).
 Proof. by rewrite -(subnDl n) -maxnE -addn_min_max addnK minnC. Qed.
@@ -765,7 +720,8 @@ Lemma leq_min m n1 n2 : (m <= minn n1 n2) = (m <= n1) && (m <= n2).
 Proof.
 wlog le_n21: n1 n2 / n2 <= n1.
   by case/orP: (leq_total n2 n1) => ?; last rewrite minnC andbC; auto.
-by rewrite /minn ltnNge le_n21 /= andbC; case: leqP => // /leq_trans->.
+rewrite /minn ltnNge le_n21 /=; case le_m_n1: (m <= n1) => //=.
+apply/contraFF: le_m_n1 => /leq_trans; exact.
 Qed.
 
 Lemma gtn_min m n1 n2 : (m > minn n1 n2) = (m > n1) || (m > n2).
@@ -820,6 +776,61 @@ Qed.
 Lemma minn_maxr : right_distributive minn maxn.
 Proof. by move=> m n1 n2; rewrite !(minnC m) minn_maxl. Qed.
 
+(* Comparison predicates. *)
+
+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 (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 : 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 (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 :=
+  | 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 : nat -> nat -> nat -> nat ->
+                          bool -> bool -> bool -> bool -> bool -> bool -> Set :=
+  | CompareNatLt of m < n :
+      compare_nat m n m m n n false false false true false true
+  | CompareNatGt of m > n :
+      compare_nat m n n n m m false false true false true false
+  | CompareNatEq of m = n :
+      compare_nat m n m m m m true true true true false false.
+
+Lemma ltngtP 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.
+rewrite leq_eqVlt; case: ltnP; rewrite ?(orbT, orbF) => //= lt_nm eq_nm.
+  by rewrite ltn_eqF //; constructor.
+by rewrite eq_nm (eqP eq_nm); constructor.
+Qed.
+
+(* Eliminating the idiom for structurally decreasing compare and subtract. *)
+Lemma subn_if_gt T m n F (E : T) :
+  (if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E).
+Proof.
+by have [le_nm|/eqnP-> //] := leqP; rewrite -{1}(subnK le_nm) -addSn addnK.
+Qed.
+
 (* Getting a concrete value from an abstract existence proof. *)
 
 Section ExMinn.
@@ -1872,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.