Generalizing homo-mono-morphism lemmas and extremum (#201)

8 files changed, 743 insertions, 157 deletions

diff --git a/ChangeLog b/ChangeLog
index 10e90e9..33d197a 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -4,7 +4,52 @@
 	  optimization is not strictly necessary with modern Coq versions.
 
 	* Added companion matrix of a polynomial `companionmx p` and the
-	  theorems: companionmxK, map_mx_companion and companion_map_poly
+	  theorems: companionmxK, map_mx_companion and companion_map_poly.
+
+	* Extended generic theory about monotonocity (*mono* and *homo* lemmas).
+
+	* Added: homoW_in, inj_homo_in, mono_inj_in, anti_mono_in,
+	  total_homo_mono_in, homoW, inj_homo, monoj, anti_mono,
+	  total_homo_mono.
+
+	* Extended theory about homo and mono for leq/or and Num.le
+
+	* Renamed: (together with the _in suffix counterpart)
+	  mono_inj -> incr_inj
+	  nmono_inj -> decr_inj
+	  leq_mono_inj -> incnr_inj
+	  leq_nmono_inj -> decnr_inj
+	  homo_inj_ltn_lt -> incnr_inj
+	  nhomo_inj_ltn_lt -> decnr_inj
+	  homo_inj_in_lt -> inj_homo_ltr_in
+	  nhomo_inj_in_lt -> inj_nhomo_ltr_in
+	  ltn_ltrW_homo -> ltnrW_homo
+	  ltn_ltrW_nhomo -> ltnrW_nhomo
+	  leq_lerW_mono -> lenrW_mono
+	  leq_lerW_nmono -> lenrW_nmono
+	  homo_leq_mono -> lenr_mono
+	  nhomo_leq_mono -> lenr_nmono
+	  homo_inj_lt -> inj_homo_ltr
+	  nhomo_inj_lt -> inj_nhomo_ltr
+	  homo_inj_ltn_lt -> inj_homo_ltnr
+	  nhomo_inj_ltn_lt -> inj_nhomo_ltnr
+	  homo_mono -> ler_mono
+	  nhomo_mono -> ler_nmono
+
+	* Added sorted_lt_nth, ltn_index, sorted_le_nth, leq_index.
+
+	* Generalized extremum_spec and its theory, added extremum and
+	  extremumP, generalizing arg_min for an arbitrary eqType with an
+	  order relation on it (rather than nat). Redefined arg_min and
+	  arg_max with it.
+
+	* Added [arg minr_( i < n | P ) F] and [arg maxr_( i < n | P ) F]
+	  with all their variants, following the same convention as for nat.
+
+	* Added missing contra* lemma: contra_neqN, contra_neqF,
+	  contra_neqT, contra_neq_eq, contra_eq_neq.
+
+	* Addded missing seq theorems: take_subseq, drop_subseq
 
 	* Reshuffled theorems inside files and packages:
 	  * countalg goes from the field to the algebra package
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index e6b0264..b1fa069 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -919,7 +919,7 @@ Proof. by rewrite -(mulr0z x) ler_nmulz2l. Qed.
 Lemma mulrIz x (hx : x != 0) : injective ( *~%R x).
 Proof.
 move=> y z; rewrite -![x *~ _]mulrzr => /(mulfI hx).
-by apply: mono_inj y z; apply: ler_pmulz2l.
+by apply: incr_inj y z; apply: ler_pmulz2l.
 Qed.
 
 Lemma ler_int m n : (m%:~R <= n%:~R :> R) = (m <= n).
@@ -1279,7 +1279,7 @@ Qed.
 Lemma ler_piexpz2l x (x0 : 0 < x) (x1 : x < 1) :
   {in >= 0 &, {mono (exprz x) : x y /~ x <= y}}.
 Proof.
-apply: (nhomo_mono_in (nhomo_inj_in_lt _ _)).
+apply: (ler_nmono_in (inj_nhomo_ltr_in _ _)).
   by move=> n m hn hm /=; apply: ieexprIz; rewrite // ltr_eqF.
 by apply: ler_wpiexpz2l; rewrite ?ltrW.
 Qed.
@@ -1291,7 +1291,7 @@ Proof. exact: (lerW_nmono_in (ler_piexpz2l _ _)). Qed.
 Lemma ler_niexpz2l x (x0 : 0 < x) (x1 : x < 1) :
   {in < 0 &, {mono (exprz x) : x y /~ x <= y}}.
 Proof.
-apply: (nhomo_mono_in (nhomo_inj_in_lt _ _)).
+apply: (ler_nmono_in (inj_nhomo_ltr_in _ _)).
   by move=> n m hn hm /=; apply: ieexprIz; rewrite // ltr_eqF.
 by apply: ler_wniexpz2l; rewrite ?ltrW.
 Qed.
@@ -1302,7 +1302,7 @@ Proof. exact: (lerW_nmono_in (ler_niexpz2l _ _)). Qed.
 
 Lemma ler_eexpz2l x (x1 : 1 < x) : {mono (exprz x) : x y / x <= y}.
 Proof.
-apply: (homo_mono (homo_inj_lt _ _)).
+apply: (ler_mono (inj_homo_ltr _ _)).
   by apply: ieexprIz; rewrite ?(ltr_trans ltr01) // gtr_eqF.
 by apply: ler_weexpz2l; rewrite ?ltrW.
 Qed.
@@ -1348,7 +1348,7 @@ Qed.
 Lemma ler_pexpz2r n (hn : 0 < n) :
   {in >= 0 & , {mono ((@exprz R)^~ n) : x y / x <= y}}.
 Proof.
-apply: homo_mono_in (homo_inj_in_lt _ _).
+apply: ler_mono_in (inj_homo_ltr_in _ _).
   by move=> x y hx hy /=; apply: pexpIrz; rewrite // gtr_eqF.
 by apply: ler_wpexpz2r; rewrite ltrW.
 Qed.
@@ -1360,7 +1360,7 @@ Proof. exact: lerW_mono_in (ler_pexpz2r _). Qed.
 Lemma ler_nexpz2r n (hn : n < 0) :
   {in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x <= y}}.
 Proof.
-apply: nhomo_mono_in (nhomo_inj_in_lt _ _); last first.
+apply: ler_nmono_in (inj_nhomo_ltr_in _ _); last first.
   by apply: ler_wnexpz2r; rewrite ltrW.
 by move=> x y hx hy /=; apply: pexpIrz; rewrite ?[_ \in _]ltrW ?ltr_eqF.
 Qed.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index ec932a1..a16cc45 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -129,6 +129,15 @@ Require Import bigop ssralg finset fingroup zmodp poly.
 (*   e : exterior = in [1, +oo[ or ]1; +oo[                                   *)
 (*   w : non strict (weak) monotony                                           *)
 (*                                                                            *)
+(* [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject       *)
+(*                   to the condition P (i may appear in P and M), and        *)
+(*                   provided P holds for i0.                                 *)
+(* [arg maxr_(i > i0 | P) M] == a value i maximizing M subject to P and       *)
+(*                   provided P holds for i0.                                 *)
+(* [arg minr_(i < i0 in A) M] == an i \in A minimizing M if i0 \in A.         *)
+(* [arg maxr_(i > i0 in A) M] == an i \in A maximizing M if i0 \in A.         *)
+(* [arg minr_(i < i0) M] == an i : T minimizing M, given i0 : T.              *)
+(* [arg maxr_(i > i0) M] == an i : T maximizing M, given i0 : T.              *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -1272,173 +1281,266 @@ Implicit Types m n p : nat.
 Implicit Types x y z : R.
 Implicit Types u v w : R'.
 
+(****************************************************************************)
+(* This listing of "Let"s factor out the required premices for the          *)
+(* subsequent lemmas, putting them in the context so that "done" solves the *)
+(* goals quickly                                                            *)
+(****************************************************************************)
+
+Let leqnn := leqnn.
+Let ltnE := ltn_neqAle.
+Let ltrE := @ltr_neqAle R.
+Let ltr'E := @ltr_neqAle R'.
+Let gtnE (m n : nat) : (m > n)%N = (m != n) && (m >= n)%N.
+Proof. by rewrite ltn_neqAle eq_sym. Qed.
+Let gtrE (x y : R) : (x > y) = (x != y) && (x >= y).
+Proof. by rewrite ltr_neqAle eq_sym. Qed.
+Let gtr'E (x y : R') : (x > y) = (x != y) && (x >= y).
+Proof. by rewrite ltr_neqAle eq_sym. Qed.
+Let leq_anti : antisymmetric leq.
+Proof. by move=> m n; rewrite -eqn_leq => /eqP. Qed.
+Let geq_anti : antisymmetric geq.
+Proof. by move=> m n; rewrite -eqn_leq => /eqP. Qed.
+Let ler_antiR := @ler_anti R.
+Let ler_antiR' := @ler_anti R'.
+Let ger_antiR : antisymmetric (>=%R : rel R).
+Proof. by move=> ??; rewrite andbC; apply: ler_anti. Qed.
+Let ger_antiR' : antisymmetric (>=%R : rel R').
+Proof. by move=> ??; rewrite andbC; apply: ler_anti. Qed.
+Let leq_total := leq_total.
+Let geq_total : total geq.
+Proof. by move=> m n; apply: leq_total. Qed.
+
 Section AcrossTypes.
 
 Variable D D' : pred R.
 Variable (f : R -> R').
 
 Lemma ltrW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y}.
-Proof. by move=> mf x y /=; rewrite ler_eqVlt => /orP[/eqP->|/mf/ltrW]. Qed.
+Proof. exact: homoW. Qed.
 
 Lemma ltrW_nhomo : {homo f : x y /~ x < y} -> {homo f : x y /~ x <= y}.
-Proof. by move=> mf x y /=; rewrite ler_eqVlt => /orP[/eqP->|/mf/ltrW]. Qed.
+Proof. exact: homoW. Qed.
 
-Lemma homo_inj_lt :
+Lemma inj_homo_ltr :
   injective f -> {homo f : x y / x <= y} -> {homo f : x y / x < y}.
-Proof.
-by move=> fI mf x y /= hxy; rewrite ltr_neqAle (inj_eq fI) mf (ltr_eqF, ltrW).
-Qed.
+Proof. exact: inj_homo. Qed.
 
-Lemma nhomo_inj_lt :
+Lemma inj_nhomo_ltr :
   injective f -> {homo f : x y /~ x <= y} -> {homo f : x y /~ x < y}.
-Proof.
-by move=> fI mf x y /= hxy; rewrite ltr_neqAle (inj_eq fI) mf (gtr_eqF, ltrW).
-Qed.
+Proof. exact: inj_homo. Qed.
 
-Lemma mono_inj : {mono f : x y / x <= y} -> injective f.
-Proof. by move=> mf x y /eqP; rewrite eqr_le !mf -eqr_le=> /eqP. Qed.
+Lemma incr_inj : {mono f : x y / x <= y} -> injective f.
+Proof. exact: mono_inj. Qed.
 
-Lemma nmono_inj : {mono f : x y /~ x <= y} -> injective f.
-Proof. by move=> mf x y /eqP; rewrite eqr_le !mf -eqr_le=> /eqP. Qed.
+Lemma decr_inj : {mono f : x y /~ x <= y} -> injective f.
+Proof. exact: mono_inj. Qed.
 
 Lemma lerW_mono : {mono f : x y / x <= y} -> {mono f : x y / x < y}.
-Proof.
-by move=> mf x y /=; rewrite !ltr_neqAle mf inj_eq //; apply: mono_inj.
-Qed.
+Proof. exact: anti_mono. Qed.
 
 Lemma lerW_nmono : {mono f : x y /~ x <= y} -> {mono f : x y /~ x < y}.
-Proof.
-by move=> mf x y /=; rewrite !ltr_neqAle mf eq_sym inj_eq //; apply: nmono_inj.
-Qed.
+Proof. exact: anti_mono. Qed.
 
 (* Monotony in D D' *)
 Lemma ltrW_homo_in :
   {in D & D', {homo f : x y / x < y}} -> {in D & D', {homo f : x y / x <= y}}.
-Proof.
-by move=> mf x y hx hy /=; rewrite ler_eqVlt => /orP[/eqP->|/mf/ltrW] //; apply.
-Qed.
+Proof. exact: homoW_in. Qed.
 
 Lemma ltrW_nhomo_in :
   {in D & D', {homo f : x y /~ x < y}} -> {in D & D', {homo f : x y /~ x <= y}}.
-Proof.
-by move=> mf x y hx hy /=; rewrite ler_eqVlt => /orP[/eqP->|/mf/ltrW] //; apply.
-Qed.
+Proof. exact: homoW_in. Qed.
 
-Lemma homo_inj_in_lt :
+Lemma inj_homo_ltr_in :
     {in D & D', injective f} ->  {in D & D', {homo f : x y / x <= y}} ->
   {in D & D', {homo f : x y / x < y}}.
-Proof.
-move=> fI mf x y hx hy /= hxy; rewrite ltr_neqAle; apply/andP; split.
-  by apply: contraTN hxy => /eqP /fI -> //; rewrite ltrr.
-by rewrite mf // (ltr_eqF, ltrW).
-Qed.
+Proof. exact: inj_homo_in. Qed.
 
-Lemma nhomo_inj_in_lt :
+Lemma inj_nhomo_ltr_in :
     {in D & D', injective f} -> {in D & D', {homo f : x y /~ x <= y}} ->
   {in D & D', {homo f : x y /~ x < y}}.
-Proof.
-move=> fI mf x y hx hy /= hxy; rewrite ltr_neqAle; apply/andP; split.
-  by apply: contraTN hxy => /eqP /fI -> //; rewrite ltrr.
-by rewrite mf // (gtr_eqF, ltrW).
-Qed.
+Proof. exact: inj_homo_in. Qed.
 
-Lemma mono_inj_in : {in D &, {mono f : x y / x <= y}} -> {in D &, injective f}.
-Proof.
-by move=> mf x y hx hy /= /eqP; rewrite eqr_le !mf // -eqr_le => /eqP.
-Qed.
+Lemma incr_inj_in : {in D &, {mono f : x y / x <= y}} ->
+   {in D &, injective f}.
+Proof. exact: mono_inj_in. Qed.
 
-Lemma nmono_inj_in :
+Lemma decr_inj_in :
   {in D &, {mono f : x y /~ x <= y}} -> {in D &, injective f}.
-Proof.
-by move=> mf x y hx hy /= /eqP; rewrite eqr_le !mf // -eqr_le => /eqP.
-Qed.
+Proof. exact: mono_inj_in. Qed.
 
 Lemma lerW_mono_in :
   {in D &, {mono f : x y / x <= y}} -> {in D &, {mono f : x y / x < y}}.
-Proof.
-move=> mf x y hx hy /=; rewrite !ltr_neqAle mf // (@inj_in_eq _ _ D) //.
-exact: mono_inj_in.
-Qed.
+Proof. exact: anti_mono_in. Qed.
 
 Lemma lerW_nmono_in :
   {in D &, {mono f : x y /~ x <= y}} -> {in D &, {mono f : x y /~ x < y}}.
-Proof.
-move=> mf x y hx hy /=; rewrite !ltr_neqAle mf // eq_sym (@inj_in_eq _ _ D) //.
-exact: nmono_inj_in.
-Qed.
+Proof. exact: anti_mono_in. Qed.
 
 End AcrossTypes.
 
 Section NatToR.
 
+Variable D D' : pred nat.
 Variable (f : nat -> R).
 
-Lemma ltn_ltrW_homo :
-    {homo f : m n / (m < n)%N >-> m < n} ->
+Lemma ltnrW_homo : {homo f : m n / (m < n)%N >-> m < n} ->
   {homo f : m n / (m <= n)%N >-> m <= n}.
-Proof. by move=> mf m n /=; rewrite leq_eqVlt => /orP[/eqP->|/mf/ltrW //]. Qed.
+Proof. exact: homoW. Qed.
 
-Lemma ltn_ltrW_nhomo :
-    {homo f : m n / (n < m)%N >-> m < n} ->
+Lemma ltnrW_nhomo : {homo f : m n / (n < m)%N >-> m < n} ->
   {homo f : m n / (n <= m)%N >-> m <= n}.
-Proof. by move=> mf m n /=; rewrite leq_eqVlt => /orP[/eqP->|/mf/ltrW//]. Qed.
+Proof. exact: homoW. Qed.
 
-Lemma homo_inj_ltn_lt :
-    injective f -> {homo f : m n / (m <= n)%N >-> m <= n} ->
+Lemma inj_homo_ltnr : injective f ->
+  {homo f : m n / (m <= n)%N >-> m <= n} ->
   {homo f : m n / (m < n)%N >-> m < n}.
-Proof.
-move=> fI mf m n /= hmn.
-by rewrite ltr_neqAle (inj_eq fI) mf ?neq_ltn ?hmn ?orbT // ltnW.
-Qed.
+Proof. exact: inj_homo. Qed.
 
-Lemma nhomo_inj_ltn_lt :
-    injective f -> {homo f : m n / (n <= m)%N >-> m <= n} ->
+Lemma inj_nhomo_ltnr : injective f ->
+  {homo f : m n / (n <= m)%N >-> m <= n} ->
   {homo f : m n / (n < m)%N >-> m < n}.
-Proof.
-move=> fI mf m n /= hmn; rewrite ltr_def (inj_eq fI).
-by rewrite mf ?neq_ltn ?hmn // ltnW.
-Qed.
+Proof. exact: inj_homo. Qed.
 
-Lemma leq_mono_inj : {mono f : m n / (m <= n)%N >-> m <= n} -> injective f.
-Proof. by move=> mf m n /eqP; rewrite eqr_le !mf -eqn_leq => /eqP. Qed.
+Lemma incnr_inj : {mono f : m n / (m <= n)%N >-> m <= n} -> injective f.
+Proof. exact: mono_inj. Qed.
 
-Lemma leq_nmono_inj : {mono f : m n / (n <= m)%N >-> m <= n} -> injective f.
-Proof. by move=> mf m n /eqP; rewrite eqr_le !mf -eqn_leq => /eqP. Qed.
+Lemma decnr_inj_inj : {mono f : m n / (n <= m)%N >-> m <= n} -> injective f.
+Proof. exact: mono_inj. Qed.
 
-Lemma leq_lerW_mono :
-    {mono f : m n / (m <= n)%N >-> m <= n} ->
+Lemma lenrW_mono : {mono f : m n / (m <= n)%N >-> m <= n} ->
   {mono f : m n / (m < n)%N >-> m < n}.
-Proof.
-move=> mf m n /=; rewrite !ltr_neqAle mf inj_eq ?ltn_neqAle 1?eq_sym //.
-exact: leq_mono_inj.
-Qed.
+Proof. exact: anti_mono. Qed.
 
-Lemma leq_lerW_nmono :
-    {mono f : m n / (n <= m)%N >-> m <= n} ->
+Lemma lenrW_nmono : {mono f : m n / (n <= m)%N >-> m <= n} ->
   {mono f : m n / (n < m)%N >-> m < n}.
-Proof.
-move=> mf x y /=; rewrite ltr_neqAle mf eq_sym inj_eq ?ltn_neqAle 1?eq_sym //.
-exact: leq_nmono_inj.
-Qed.
+Proof. exact: anti_mono. Qed.
 
-Lemma homo_leq_mono :
-    {homo f : m n / (m < n)%N >-> m < n} ->
+Lemma lenr_mono : {homo f : m n / (m < n)%N >-> m < n} ->
    {mono f : m n / (m <= n)%N >-> m <= n}.
-Proof.
-move=> mf m n /=; case: leqP; last by move=> /mf /ltr_geF.
-by rewrite leq_eqVlt => /orP[/eqP->|/mf/ltrW //]; rewrite lerr.
-Qed.
+Proof. exact: total_homo_mono. Qed.
 
-Lemma nhomo_leq_mono :
-    {homo f : m n / (n < m)%N >-> m < n} ->
+Lemma lenr_nmono : {homo f : m n / (n < m)%N >-> m < n} ->
   {mono f : m n / (n <= m)%N >-> m <= n}.
-Proof.
-move=> mf m n /=; case: leqP; last by move=> /mf /ltr_geF.
-by rewrite leq_eqVlt => /orP[/eqP->|/mf/ltrW //]; rewrite lerr.
-Qed.
+Proof. exact: total_homo_mono. Qed.
+
+Lemma ltnrW_homo_in : {in D & D', {homo f : m n / (m < n)%N >-> m < n}} ->
+  {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}}.
+Proof. exact: homoW_in. Qed.
+
+Lemma ltnrW_nhomo_in : {in D & D', {homo f : m n / (n < m)%N >-> m < n}} ->
+  {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}}.
+Proof. exact: homoW_in. Qed.
+
+Lemma inj_homo_ltnr_in : {in D & D', injective f} ->
+  {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}} ->
+  {in D & D', {homo f : m n / (m < n)%N >-> m < n}}.
+Proof. exact: inj_homo_in. Qed.
+
+Lemma inj_nhomo_ltnr_in : {in D & D', injective f} ->
+  {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}} ->
+  {in D & D', {homo f : m n / (n < m)%N >-> m < n}}.
+Proof. exact: inj_homo_in. Qed.
+
+Lemma incnr_inj_in : {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} ->
+  {in D &, injective f}.
+Proof. exact: mono_inj_in. Qed.
+
+Lemma decnr_inj_inj_in : {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} ->
+  {in D &, injective f}.
+Proof. exact: mono_inj_in. Qed.
+
+Lemma lenrW_mono_in : {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} ->
+  {in D &, {mono f : m n / (m < n)%N >-> m < n}}.
+Proof. exact: anti_mono_in. Qed.
+
+Lemma lenrW_nmono_in : {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} ->
+  {in D &, {mono f : m n / (n < m)%N >-> m < n}}.
+Proof. exact: anti_mono_in. Qed.
+
+Lemma lenr_mono_in : {in D &, {homo f : m n / (m < n)%N >-> m < n}} ->
+   {in D &, {mono f : m n / (m <= n)%N >-> m <= n}}.
+Proof. exact: total_homo_mono_in. Qed.
+
+Lemma lenr_nmono_in : {in D &, {homo f : m n / (n < m)%N >-> m < n}} ->
+  {in D &, {mono f : m n / (n <= m)%N >-> m <= n}}.
+Proof. exact: total_homo_mono_in. Qed.
 
 End NatToR.
 
+Section RToNat.
+
+Variable D D' : pred R.
+Variable (f : R -> nat).
+
+Lemma ltrnW_homo : {homo f : m n / m < n >-> (m < n)%N} ->
+  {homo f : m n / m <= n >-> (m <= n)%N}.
+Proof. exact: homoW. Qed.
+
+Lemma ltrnW_nhomo : {homo f : m n / n < m >-> (m < n)%N} ->
+  {homo f : m n / n <= m >-> (m <= n)%N}.
+Proof. exact: homoW. Qed.
+
+Lemma inj_homo_ltrn : injective f ->
+  {homo f : m n / m <= n >-> (m <= n)%N} ->
+  {homo f : m n / m < n >-> (m < n)%N}.
+Proof. exact: inj_homo. Qed.
+
+Lemma inj_nhomo_ltrn : injective f ->
+  {homo f : m n / n <= m >-> (m <= n)%N} ->
+  {homo f : m n / n < m >-> (m < n)%N}.
+Proof. exact: inj_homo. Qed.
+
+Lemma incrn_inj : {mono f : m n / m <= n >-> (m <= n)%N} -> injective f.
+Proof. exact: mono_inj. Qed.
+
+Lemma decrn_inj : {mono f : m n / n <= m >-> (m <= n)%N} -> injective f.
+Proof. exact: mono_inj. Qed.
+
+Lemma lernW_mono : {mono f : m n / m <= n >-> (m <= n)%N} ->
+  {mono f : m n / m < n >-> (m < n)%N}.
+Proof. exact: anti_mono. Qed.
+
+Lemma lernW_nmono : {mono f : m n / n <= m >-> (m <= n)%N} ->
+  {mono f : m n / n < m >-> (m < n)%N}.
+Proof. exact: anti_mono. Qed.
+
+Lemma ltrnW_homo_in : {in D & D', {homo f : m n / m < n >-> (m < n)%N}} ->
+  {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}}.
+Proof. exact: homoW_in. Qed.
+
+Lemma ltrnW_nhomo_in : {in D & D', {homo f : m n / n < m >-> (m < n)%N}} ->
+  {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}}.
+Proof. exact: homoW_in. Qed.
+
+Lemma inj_homo_ltrn_in : {in D & D', injective f} ->
+  {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}} ->
+  {in D & D', {homo f : m n / m < n >-> (m < n)%N}}.
+Proof. exact: inj_homo_in. Qed.
+
+Lemma inj_nhomo_ltrn_in : {in D & D', injective f} ->
+  {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}} ->
+  {in D & D', {homo f : m n / n < m >-> (m < n)%N}}.
+Proof. exact: inj_homo_in. Qed.
+
+Lemma incrn_inj_in : {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} ->
+  {in D &, injective f}.
+Proof. exact: mono_inj_in. Qed.
+
+Lemma decrn_inj_in : {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} ->
+  {in D &, injective f}.
+Proof. exact: mono_inj_in. Qed.
+
+Lemma lernW_mono_in : {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} ->
+  {in D &, {mono f : m n / m < n >-> (m < n)%N}}.
+Proof. exact: anti_mono_in. Qed.
+
+Lemma lernW_nmono_in : {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} ->
+  {in D &, {mono f : m n / n < m >-> (m < n)%N}}.
+Proof. exact: anti_mono_in. Qed.
+
+End RToNat.
+
 End NumIntegralDomainMonotonyTheory.
 
 Section NumDomainOperationTheory.
@@ -1975,7 +2077,7 @@ Lemma ltr_pmuln2r n : (0 < n)%N -> {mono (@GRing.natmul R)^~ n : x y / x < y}.
 Proof. by move/ler_pmuln2r/lerW_mono. Qed.
 
 Lemma pmulrnI n : (0 < n)%N -> injective ((@GRing.natmul R)^~ n).
-Proof. by move/ler_pmuln2r/mono_inj. Qed.
+Proof. by move/ler_pmuln2r/incr_inj. Qed.
 
 Lemma eqr_pmuln2r n : (0 < n)%N -> {mono (@GRing.natmul R)^~ n : x y / x == y}.
 Proof. by move/pmulrnI/inj_eq. Qed.
@@ -2054,7 +2156,7 @@ Qed.
 
 Lemma ltr_pmuln2l x :
   0 < x -> {mono (@GRing.natmul R x) : m n / (m < n)%N >-> m < n}.
-Proof. by move=> x_gt0; apply: leq_lerW_mono (ler_pmuln2l _). Qed.
+Proof. by move=> x_gt0; apply: lenrW_mono (ler_pmuln2l _). Qed.
 
 Lemma ler_nmuln2l x :
   x < 0 -> {mono (@GRing.natmul R x) : m n / (n <= m)%N >-> m <= n}.
@@ -2064,7 +2166,7 @@ Qed.
 
 Lemma ltr_nmuln2l x :
   x < 0 -> {mono (@GRing.natmul R x) : m n / (n < m)%N >-> m < n}.
-Proof. by move=> x_lt0; apply: leq_lerW_nmono (ler_nmuln2l _). Qed.
+Proof. by move=> x_lt0; apply: lenrW_nmono (ler_nmuln2l _). Qed.
 
 Lemma ler_nat m n : (m%:R <= n%:R :> R) = (m <= n)%N.
 Proof. by rewrite ler_pmuln2l. Qed.
@@ -2470,28 +2572,28 @@ Qed.
 Lemma ler_iexpn2l x :
   0 < x -> x < 1 -> {mono (GRing.exp x) : m n / (n <= m)%N >-> m <= n}.
 Proof.
-move=> xgt0 xlt1; apply: (nhomo_leq_mono (nhomo_inj_ltn_lt _ _)); last first.
+move=> xgt0 xlt1; apply: (lenr_nmono (inj_nhomo_ltnr _ _)); last first.
   by apply: ler_wiexpn2l; rewrite ltrW.
 by apply: ieexprIn; rewrite ?ltr_eqF ?ltr_cpable.
 Qed.
 
 Lemma ltr_iexpn2l x :
   0 < x -> x < 1 -> {mono (GRing.exp x) : m n / (n < m)%N >-> m < n}.
-Proof. by move=> xgt0 xlt1; apply: (leq_lerW_nmono (ler_iexpn2l _ _)). Qed.
+Proof. by move=> xgt0 xlt1; apply: (lenrW_nmono (ler_iexpn2l _ _)). Qed.
 
 Definition lter_iexpn2l := (ler_iexpn2l, ltr_iexpn2l).
 
 Lemma ler_eexpn2l x :
   1 < x -> {mono (GRing.exp x) : m n / (m <= n)%N >-> m <= n}.
 Proof.
-move=> xgt1; apply: (homo_leq_mono (homo_inj_ltn_lt _ _)); last first.
+move=> xgt1; apply: (lenr_mono (inj_homo_ltnr _ _)); last first.
   by apply: ler_weexpn2l; rewrite ltrW.
 by apply: ieexprIn; rewrite ?gtr_eqF ?gtr_cpable //; apply: ltr_trans xgt1.
 Qed.
 
 Lemma ltr_eexpn2l x :
   1 < x -> {mono (GRing.exp x) : m n / (m < n)%N >-> m < n}.
-Proof. by move=> xgt1; apply: (leq_lerW_mono (ler_eexpn2l _)). Qed.
+Proof. by move=> xgt1; apply: (lenrW_mono (ler_eexpn2l _)). Qed.
 
 Definition lter_eexpn2l := (ler_eexpn2l, ltr_eexpn2l).
 
@@ -2535,7 +2637,7 @@ Qed.
 Definition lter_pexpn2r := (ler_pexpn2r, ltr_pexpn2r).
 
 Lemma pexpIrn n : (0 < n)%N -> {in nneg &, injective ((@GRing.exp R)^~ n)}.
-Proof. by move=> n_gt0; apply: mono_inj_in (ler_pexpn2r _). Qed.
+Proof. by move=> n_gt0; apply: incr_inj_in (ler_pexpn2r _). Qed.
 
 (* expr and ler/ltr *)
 Lemma expr_le1 n x : (0 < n)%N -> 0 <= x -> (x ^+ n <= 1) = (x <= 1).
@@ -2971,25 +3073,26 @@ Lemma mono_in_lerif (A : pred R) (f : R -> R) C :
    {in A &, {mono f : x y / x <= y}} ->
   {in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)}.
 Proof.
-by move=> mf x y Ax Ay; rewrite /lerif mf ?(inj_in_eq (mono_inj_in mf)).
+by move=> mf x y Ax Ay; rewrite /lerif mf ?(inj_in_eq (incr_inj_in mf)).
 Qed.
 
 Lemma mono_lerif (f : R -> R) C :
     {mono f : x y / x <= y} ->
   forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C).
-Proof. by move=> mf x y; rewrite /lerif mf (inj_eq (mono_inj _)). Qed.
+Proof. by move=> mf x y; rewrite /lerif mf (inj_eq (incr_inj _)). Qed.
 
 Lemma nmono_in_lerif (A : pred R) (f : R -> R) C :
     {in A &, {mono f : x y /~ x <= y}} ->
   {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)}.
 Proof.
-by move=> mf x y Ax Ay; rewrite /lerif eq_sym mf ?(inj_in_eq (nmono_inj_in mf)).
+move=> mf x y Ax Ay; rewrite /lerif eq_sym mf //.
+by rewrite ?(inj_in_eq (decr_inj_in mf)).
 Qed.
 
 Lemma nmono_lerif (f : R -> R) C :
     {mono f : x y /~ x <= y} ->
   forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C).
-Proof. by move=> mf x y; rewrite /lerif eq_sym mf ?(inj_eq (nmono_inj mf)). Qed.
+Proof. by move=> mf x y; rewrite /lerif eq_sym mf ?(inj_eq (decr_inj mf)). Qed.
 
 Lemma lerif_subLR x y z C : (x - y <= z ?= iff C) = (x <= z + y ?= iff C).
 Proof. by rewrite /lerif !eqr_le ler_subr_addr ler_subl_addr. Qed.
@@ -3158,7 +3261,7 @@ Arguments nmono_lerif [R f C].
 
 Section NumDomainMonotonyTheoryForReals.
 
-Variables (R R' : numDomainType) (D : pred R) (f : R -> R').
+Variables (R R' : numDomainType) (D : pred R) (f : R -> R') (f' : R -> nat).
 Implicit Types (m n p : nat) (x y z : R) (u v w : R').
 
 Lemma real_mono :
@@ -3177,7 +3280,6 @@ move=> mf x y xR yR /=; have [lt_xy|le_yx] := real_ltrP xR yR.
 by rewrite ltrW_nhomo.
 Qed.
 
-(* GG: Domain should precede condition. *)
 Lemma real_mono_in :
     {in D &, {homo f : x y / x < y}} ->
   {in [pred x in D | x \is real] &, {mono f : x y / x <= y}}.
@@ -3196,6 +3298,38 @@ have [lt_xy|le_yx] := real_ltrP xR yR; last by rewrite (ltrW_nhomo_in Dmf).
 by rewrite ltr_geF ?Dmf.
 Qed.
 
+Lemma realn_mono : {homo f' : x y / x < y >-> (x < y)%N} ->
+  {in real &, {mono f' : x y / x <= y >-> (x <= y)%N}}.
+Proof.
+move=> mf x y xR yR /=; have [lt_xy | le_yx] := real_lerP xR yR.
+  by rewrite ltrnW_homo.
+by rewrite ltn_geF ?mf.
+Qed.
+
+Lemma realn_nmono : {homo f' : x y / y < x >-> (x < y)%N} ->
+  {in real &, {mono f' : x y / y <= x >-> (x <= y)%N}}.
+Proof.
+move=> mf x y xR yR /=; have [lt_xy|le_yx] := real_ltrP xR yR.
+  by rewrite ltn_geF ?mf.
+by rewrite ltrnW_nhomo.
+Qed.
+
+Lemma realn_mono_in : {in D &, {homo f' : x y / x < y >-> (x < y)%N}} ->
+  {in [pred x in D | x \is real] &, {mono f' : x y / x <= y >-> (x <= y)%N}}.
+Proof.
+move=> Dmf x y /andP[hx xR] /andP[hy yR] /=.
+have [lt_xy|le_yx] := real_lerP xR yR; first by rewrite (ltrnW_homo_in Dmf).
+by rewrite ltn_geF ?Dmf.
+Qed.
+
+Lemma realn_nmono_in : {in D &, {homo f' : x y / y < x >-> (x < y)%N}} ->
+  {in [pred x in D | x \is real] &, {mono f' : x y / y <= x >-> (x <= y)%N}}.
+Proof.
+move=> Dmf x y /andP[hx xR] /andP[hy yR] /=.
+have [lt_xy|le_yx] := real_ltrP xR yR; last by rewrite (ltrnW_nhomo_in Dmf).
+by rewrite ltn_geF ?Dmf.
+Qed.
+
 End NumDomainMonotonyTheoryForReals.
 
 Section FinGroup.
@@ -3538,31 +3672,100 @@ Hint Resolve num_real : core.
 
 Section RealDomainMonotony.
 
-Variables (R : realDomainType) (R' : numDomainType) (D : pred R) (f : R -> R').
+Variables (R : realDomainType) (R' : numDomainType) (D : pred R).
+Variables (f : R -> R') (f' : R -> nat).
 Implicit Types (m n p : nat) (x y z : R) (u v w : R').
 
 Hint Resolve (@num_real R) : core.
 
-Lemma homo_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}.
+Lemma ler_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}.
 Proof. by move=> mf x y; apply: real_mono. Qed.
 
-Lemma nhomo_mono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y}.
+Lemma ler_nmono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y}.
 Proof. by move=> mf x y; apply: real_nmono. Qed.
 
-Lemma homo_mono_in :
+Lemma ler_mono_in :
   {in D &, {homo f : x y / x < y}} -> {in D &, {mono f : x y / x <= y}}.
 Proof.
 by move=> mf x y Dx Dy; apply: (real_mono_in mf); rewrite ?inE ?Dx ?Dy /=.
 Qed.
 
-Lemma nhomo_mono_in :
+Lemma ler_nmono_in :
   {in D &, {homo f : x y /~ x < y}} -> {in D &, {mono f : x y /~ x <= y}}.
 Proof.
 by move=> mf x y Dx Dy; apply: (real_nmono_in mf); rewrite ?inE ?Dx ?Dy /=.
 Qed.
 
+Lemma lern_mono : {homo f' : m n / m < n >-> (m < n)%N} ->
+   {mono f' : m n / m <= n >-> (m <= n)%N}.
+Proof. by move=> mf x y; apply: realn_mono. Qed.
+
+Lemma lern_nmono : {homo f' : m n / n < m >-> (m < n)%N} ->
+  {mono f' : m n / n <= m >-> (m <= n)%N}.
+Proof. by move=> mf x y; apply: realn_nmono. Qed.
+
+Lemma lern_mono_in : {in D &, {homo f' : m n / m < n >-> (m < n)%N}} ->
+   {in D &, {mono f' : m n / m <= n >-> (m <= n)%N}}.
+Proof.
+by move=> mf x y Dx Dy; apply: (realn_mono_in mf); rewrite ?inE ?Dx ?Dy /=.
+Qed.
+
+Lemma lern_nmono_in : {in D &, {homo f' : m n / n < m >-> (m < n)%N}} ->
+  {in D &, {mono f' : m n / n <= m >-> (m <= n)%N}}.
+Proof.
+by move=> mf x y Dx Dy; apply: (realn_nmono_in mf); rewrite ?inE ?Dx ?Dy /=.
+Qed.
+
 End RealDomainMonotony.
 
+Section RealDomainArgExtremum.
+
+Context {R : realDomainType} {I : finType} (i0 : I).
+Context (P : pred I) (F : I -> R) (Pi0 : P i0).
+
+Definition arg_minr := extremum <=%R i0 P F.
+Definition arg_maxr := extremum >=%R i0 P F.
+
+Lemma arg_minrP: extremum_spec <=%R P F arg_minr.
+Proof. by apply: extremumP => //; [apply: ler_trans|apply: ler_total]. Qed.
+
+Lemma arg_maxrP: extremum_spec >=%R P F arg_maxr.
+Proof.
+apply: extremumP => //; first exact: lerr.
+  by move=> ??? /(ler_trans _) le /le.
+by move=> ??; apply: ler_total.
+Qed.
+
+End RealDomainArgExtremum.
+
+Notation "[ 'arg' 'minr_' ( i < i0 | P ) F ]" :=
+    (arg_minr i0 (fun i => P%B) (fun i => F))
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'minr_' ( i  <  i0  |  P )  F ]") : form_scope.
+
+Notation "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]" :=
+    [arg minr_(i < i0 | i \in A) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'minr_' ( i  <  i0  'in'  A )  F ]") : form_scope.
+
+Notation "[ 'arg' 'minr_' ( i < i0 ) F ]" := [arg minr_(i < i0 | true) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'minr_' ( i  <  i0 )  F ]") : form_scope.
+
+Notation "[ 'arg' 'maxr_' ( i > i0 | P ) F ]" :=
+     (arg_maxr i0 (fun i => P%B) (fun i => F))
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'maxr_' ( i  >  i0  |  P )  F ]") : form_scope.
+
+Notation "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]" :=
+    [arg maxr_(i > i0 | i \in A) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'maxr_' ( i  >  i0  'in'  A )  F ]") : form_scope.
+
+Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg'  'maxr_' ( i  >  i0 ) F ]") : form_scope.
+
 Section RealDomainOperations.
 
 (* sgr section *)
@@ -4107,7 +4310,7 @@ Qed.
 
 Lemma ler_psqrt : {in @pos R &, {mono sqrt : a b / a <= b}}.
 Proof.
-apply: homo_mono_in => x y x_gt0 y_gt0.
+apply: ler_mono_in => x y x_gt0 y_gt0.
 rewrite !ltr_neqAle => /andP[neq_xy le_xy].
 by rewrite ler_wsqrtr // eqr_sqrt ?ltrW // neq_xy.
 Qed.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 58ef844..13ba8ca 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -230,12 +230,27 @@ Proof. by move=> imp /eqP; apply: contraTF. Qed.
 Lemma contra_eqT b x y : (~~ b -> x != y) -> x = y -> b.
 Proof. by move=> imp /eqP; apply: contraLR. Qed.
 
+Lemma contra_neqN b x y : (b -> x = y) -> x != y -> ~~ b.
+Proof. by move=> imp; apply: contraNN => /imp->. Qed.
+
+Lemma contra_neqF b x y : (b -> x = y) -> x != y -> b = false.
+Proof. by move=> imp; apply: contraNF => /imp->. Qed.
+
+Lemma contra_neqT b x y : (~~ b -> x = y) -> x != y -> b.
+Proof. by move=> imp; apply: contraNT => /imp->. Qed.
+
 Lemma contra_eq z1 z2 x1 x2 : (x1 != x2 -> z1 != z2) -> z1 = z2 -> x1 = x2.
 Proof. by move=> imp /eqP; apply: contraTeq. Qed.
 
 Lemma contra_neq z1 z2 x1 x2 : (x1 = x2 -> z1 = z2) -> z1 != z2 -> x1 != x2.
 Proof. by move=> imp; apply: contraNneq => /imp->. Qed.
 
+Lemma contra_neq_eq z1 z2 x1 x2 : (x1 != x2 -> z1 = z2) -> z1 != z2 -> x1 = x2.
+Proof. by move=> imp; apply: contraNeq => /imp->. Qed.
+
+Lemma contra_eq_neq z1 z2 x1 x2 : (z1 = z2 -> x1 != x2) -> x1 = x2 -> z1 != z2.
+Proof. by move=> imp; apply: contra_eqN => /eqP /imp. Qed.
+
 Lemma memPn A x : reflect {in A, forall y, y != x} (x \notin A).
 Proof.
 apply: (iffP idP) => [notDx y | notDx]; first by apply: contraTneq => ->.
@@ -882,3 +897,103 @@ End SumEqType.
 
 Arguments sum_eq {T1 T2} !u !v.
 Arguments sum_eqP {T1 T2 x y}.
+
+Section MonoHomoTheory.
+
+Variables (aT rT : eqType) (f : aT -> rT).
+Variables (aR aR' : rel aT) (rR rR' : rel rT).
+
+Hypothesis aR_refl : reflexive aR.
+Hypothesis rR_refl : reflexive rR.
+Hypothesis aR'E : forall x y, aR' x y = (x != y) && (aR x y).
+Hypothesis rR'E : forall x y, rR' x y = (x != y) && (rR x y).
+
+Let aRE x y : aR x y = (x == y) || (aR' x y).
+Proof. by rewrite aR'E; case: (altP eqP) => //= ->; apply: aR_refl. Qed.
+Let rRE x y : rR x y = (x == y) || (rR' x y).
+Proof. by rewrite rR'E; case: (altP eqP) => //= ->; apply: rR_refl. Qed.
+
+Section InDom.
+Variable D : pred aT.
+
+Section DifferentDom.
+Variable D' : pred aT.
+
+Lemma homoW_in : {in D & D', {homo f : x y / aR' x y >-> rR' x y}} ->
+                 {in D & D', {homo f : x y / aR x y >-> rR x y}}.
+Proof.
+move=> mf x y xD yD /=; rewrite aRE => /orP[/eqP->|/mf];
+by rewrite rRE ?eqxx // orbC => ->.
+Qed.
+
+Lemma inj_homo_in : {in D & D', injective f} ->
+  {in D & D', {homo f : x y / aR x y >-> rR x y}} ->
+  {in D & D', {homo f : x y / aR' x y >-> rR' x y}}.
+Proof.
+move=> fI mf x y xD yD /=; rewrite aR'E rR'E => /andP[neq_xy xy].
+by rewrite mf ?andbT //; apply: contra_neq neq_xy => /fI; apply.
+Qed.
+
+End DifferentDom.
+
+Hypothesis aR_anti : antisymmetric aR.
+Hypothesis rR_anti : antisymmetric rR.
+
+Lemma mono_inj_in : {in D &, {mono f : x y / aR x y >-> rR x y}} ->
+                 {in D &, injective f}.
+Proof. by move=> mf x y ?? eqf; apply/aR_anti; rewrite -!mf// eqf rR_refl. Qed.
+
+Lemma anti_mono_in : {in D &, {mono f : x y / aR x y >-> rR x y}} ->
+                     {in D &, {mono f : x y / aR' x y >-> rR' x y}}.
+Proof.
+move=> mf x y ??; rewrite rR'E aR'E mf// (@inj_in_eq _ _ D)//.
+exact: mono_inj_in.
+Qed.
+
+Lemma total_homo_mono_in : total aR ->
+    {in D &, {homo f : x y / aR' x y >-> rR' x y}} ->
+   {in D &, {mono f : x y / aR x y >-> rR x y}}.
+Proof.
+move=> aR_tot mf x y xD yD.
+have [->|neq_xy] := altP (x =P y); first by rewrite ?eqxx ?aR_refl ?rR_refl.
+have [xy|] := (boolP (aR x y)); first by rewrite rRE mf ?orbT// aR'E neq_xy.
+have /orP [->//|] := aR_tot x y.
+rewrite aRE eq_sym (negPf neq_xy) /= => /mf -/(_ yD xD).
+rewrite rR'E => /andP[Nfxfy fyfx] _; apply: contra_neqF Nfxfy => fxfy.
+by apply/rR_anti; rewrite fyfx fxfy.
+Qed.
+
+End InDom.
+
+Let D := @predT aT.
+
+Lemma homoW : {homo f : x y / aR' x y >-> rR' x y} ->
+                 {homo f : x y / aR x y >-> rR x y}.
+Proof. by move=> mf ???; apply: (@homoW_in D D) => // ????; apply: mf. Qed.
+
+Lemma inj_homo : injective f ->
+  {homo f : x y / aR x y >-> rR x y} ->
+  {homo f : x y / aR' x y >-> rR' x y}.
+Proof.
+by move=> fI mf ???; apply: (@inj_homo_in D D) => //????; [apply: fI|apply: mf].
+Qed.
+
+Hypothesis aR_anti : antisymmetric aR.
+Hypothesis rR_anti : antisymmetric rR.
+
+Lemma mono_inj : {mono f : x y / aR x y >-> rR x y} -> injective f.
+Proof. by move=> mf x y eqf; apply/aR_anti; rewrite -!mf eqf rR_refl. Qed.
+
+Lemma anti_mono : {mono f : x y / aR x y >-> rR x y} ->
+                  {mono f : x y / aR' x y >-> rR' x y}.
+Proof. by move=> mf x y; rewrite rR'E aR'E mf inj_eq //; apply: mono_inj. Qed.
+
+Lemma total_homo_mono : total aR ->
+    {homo f : x y / aR' x y >-> rR' x y} ->
+   {mono f : x y / aR x y >-> rR x y}.
+Proof.
+move=> /(@total_homo_mono_in D rR_anti) hmf hf => x y.
+by apply: hmf => // ?? _ _; apply: hf.
+Qed.
+
+End MonoHomoTheory.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 06aca24..2544ab6 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -2,7 +2,7 @@
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq choice.
+Require Import ssrfun ssrbool eqtype ssrnat seq choice path.
 
 (******************************************************************************)
 (*    The Finite interface describes Types with finitely many elements,       *)
@@ -133,15 +133,22 @@ Require Import ssrfun ssrbool eqtype ssrnat seq choice.
 (*   [pick x | P & Q] := [pick x | P & Q].                                    *)
 (* [pick x in A | P & Q] := [pick x | P & Q].                                 *)
 (* and (un)typed variants [pick x : T | P], [pick x : T in A], [pick x], etc. *)
-(* [arg min_(i < i0 | P) M] == a value of i : T minimizing M : nat, subject   *)
+(* [arg min_(i < i0 | P) M] == a value i : T minimizing M : nat, subject      *)
 (*                   to the condition P (i may appear in P and M), and        *)
 (*                   provided P holds for i0.                                 *)
-(* [arg max_(i > i0 | P) M] == a value of i maximizing M subject to P and     *)
+(* [arg max_(i > i0 | P) M] == a value i maximizing M subject to P and        *)
 (*                   provided P holds for i0.                                 *)
 (* [arg min_(i < i0 in A) M] == an i \in A minimizing M if i0 \in A.          *)
 (* [arg max_(i > i0 in A) M] == an i \in A maximizing M if i0 \in A.          *)
 (* [arg min_(i < i0) M] == an i : T minimizing M, given i0 : T.               *)
 (* [arg max_(i > i0) M] == an i : T maximizing M, given i0 : T.               *)
+(*   These are special instances of                                           *)
+(* [arg[ord]_(i < i0 | P) F] == a value i : I, minimizing F wrt ord : rel T   *)
+(*                              such that for all j : T, ord (F i) (F j)      *)
+(*                              subject to the condition P, and provided P i0 *)
+(*                              where I : finType, T : eqType and F : I -> T  *)
+(* [arg[ord]_(i < i0 in A) F] == an i \in A minimizing F wrt ord, if i0 \in A.*)
+(* [arg[ord]_(i < i0) F] == an i : T minimizing F wrt ord, given i0 : T.      *)
 (******************************************************************************)
 
 Set Implicit Arguments.
@@ -942,47 +949,76 @@ Notation "'forall_in_ view" := (forall_inPP _ (fun _ => view))
 
 Section Extrema.
 
-Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat).
+Variant extremum_spec {T : eqType} (ord : rel T) {I : finType}
+  (P : pred I) (F : I -> T) : I -> Type :=
+  ExtremumSpec (i : I) of P i & (forall j : I, P j -> ord (F i) (F j)) :
+                   extremum_spec ord P F i.
 
-Let arg_pred ord := [pred i | P i & [forall (j | P j), ord (F i) (F j)]].
+Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I -> T) :=
+  [pred i | P i & [forall (j | P j), ord (F i) (F j)]].
 
-Definition arg_min := odflt i0 (pick (arg_pred leq)).
+Section Extremum.
 
-Definition arg_max := odflt i0 (pick (arg_pred geq)).
+Context {T : eqType} {I : finType} (ord : rel T).
+Context (i0 : I) (P : pred I) (F : I -> T).
 
-Variant extremum_spec (ord : rel nat) : I -> Type :=
-  ExtremumSpec i of P i & (forall j, P j -> ord (F i) (F j))
-    : extremum_spec ord i.
+Hypothesis ord_refl : reflexive ord.
+Hypothesis ord_trans : transitive ord.
+Hypothesis ord_total : total ord.
 
-Hypothesis Pi0 : P i0.
+Definition extremum := odflt i0 (pick (arg_pred ord P F)).
 
-Let FP n := [exists (i | P i), F i == n].
-Let FP_F i : P i -> FP (F i).
-Proof. by move=> Pi; apply/existsP; exists i; rewrite Pi /=. Qed.
-Let exFP : exists n, FP n. Proof. by exists (F i0); apply: FP_F. Qed.
+Hypothesis Pi0 : P i0.
 
-Lemma arg_minP : extremum_spec leq arg_min.
+Lemma extremumP : extremum_spec ord P F extremum.
 Proof.
-rewrite /arg_min; case: pickP => [i /andP[Pi /forallP/= min_i] | no_i].
+rewrite /extremum; case: pickP => [i /andP[Pi /'forall_implyP/= min_i] | no_i].
   by split=> // j; apply/implyP.
-case/ex_minnP: exFP => n ex_i min_i; case/pred0P: ex_i => i /=.
-apply: contraFF (no_i i) => /andP[Pi /eqP def_n]; rewrite /= Pi.
-by apply/forall_inP=> j Pj; rewrite def_n min_i ?FP_F.
+have := sort_sorted ord_total [seq F i | i <- enum P].
+set s := sort _ _ => ss; have s_gt0 : size s > 0
+   by rewrite size_sort size_map -cardE; apply/card_gt0P; exists i0.
+pose t0 := nth (F i0) s 0; have: t0 \in s by rewrite mem_nth.
+rewrite mem_sort => /mapP/sig2_eqW[it0]; rewrite mem_enum => it0P def_t0.
+have /negP[/=] := no_i it0; rewrite [P _]it0P/=; apply/'forall_implyP=> j Pj.
+have /(nthP (F i0))[k g_lt <-] : F j \in s by rewrite mem_sort map_f ?mem_enum.
+by rewrite -def_t0 sorted_le_nth.
 Qed.
 
-Lemma arg_maxP : extremum_spec geq arg_max.
+End Extremum.
+
+Notation "[ 'arg[' ord ]_( i < i0 | P ) F ]" :=
+    (extremum ord i0 (fun i => P%B) (fun i => F))
+  (at level 0, ord, i, i0 at level 10,
+   format "[ 'arg[' ord ]_( i  <  i0  |  P )  F ]") : form_scope.
+
+Notation "[ 'arg[' ord ]_( i < i0 'in' A ) F ]" :=
+    [arg[ord]_(i < i0 | i \in A) F]
+  (at level 0, ord, i, i0 at level 10,
+   format "[ 'arg[' ord ]_( i  <  i0  'in'  A )  F ]") : form_scope.
+
+Notation "[ 'arg[' ord ]_( i < i0 ) F ]" := [arg[ord]_(i < i0 | true) F]
+  (at level 0, ord, i, i0 at level 10,
+   format "[ 'arg[' ord ]_( i  <  i0 )  F ]") : form_scope.
+
+Section ArgMinMax.
+
+Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat) (Pi0 : P i0).
+
+Definition arg_min := extremum leq i0 P F.
+Definition arg_max := extremum geq i0 P F.
+
+Lemma arg_minP : extremum_spec leq P F arg_min.
+Proof. by apply: extremumP => //; [apply: leq_trans|apply: leq_total]. Qed.
+
+Lemma arg_maxP : extremum_spec geq P F arg_max.
 Proof.
-rewrite /arg_max; case: pickP => [i /andP[Pi /forall_inP/= max_i] | no_i].
-  by split=> // j; apply/implyP.
-have (n): FP n -> n <= foldr maxn 0 (map F (enum P)).
-  case/existsP=> i; rewrite -[P i]mem_enum andbC /= => /andP[/eqP <-].
-  elim: (enum P) => //= j e IHe; rewrite leq_max orbC !inE.
-  by case/predU1P=> [-> | /IHe-> //]; rewrite leqnn orbT.
-case/ex_maxnP=> // n ex_i max_i; case/pred0P: ex_i => i /=.
-apply: contraFF (no_i i) => /andP[Pi def_n]; rewrite /= Pi.
-by apply/forall_inP=> j Pj; rewrite (eqP def_n) max_i ?FP_F.
+apply: extremumP => //; first exact: leqnn.
+  by move=> n m p mn np; apply: leq_trans mn.
+by move=> ??; apply: leq_total.
 Qed.
 
+End ArgMinMax.
+
 End Extrema.
 
 Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index dd67256..b6bc4ed 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -890,3 +890,46 @@ End CycleArc.
 
 Prenex Implicits arc.
 
+Section Monotonicity.
+
+Variables (T : eqType) (r : rel T).
+
+Hypothesis r_trans : transitive r.
+
+Lemma sorted_lt_nth x0 (s : seq T) : sorted r s ->
+  {in [pred n | n < size s] &, {homo nth x0 s : i j / i < j >-> r i j}}.
+Proof.
+move=> s_sorted i j; rewrite -!topredE /=.
+wlog ->: i j s s_sorted / i = 0 => [/(_ 0 (j - i) (drop i s)) hw|] ilt jlt ltij.
+  move: hw; rewrite !size_drop !nth_drop addn0 subnKC ?(ltnW ltij) //.
+  by rewrite (subseq_sorted _ (drop_subseq _ _)) ?subn_gt0 ?ltn_sub2r//; apply.
+case: s ilt j jlt ltij => [|x s] //= _ [//|j] jlt _ in s_sorted *.
+by have /allP -> //= := order_path_min r_trans s_sorted; rewrite mem_nth.
+Qed.
+
+Lemma ltn_index (s : seq T) : sorted r s ->
+  {in s &, forall x y, index x s < index y s -> r x y}.
+Proof.
+case: s => [//|x0 s'] r_sorted x y xs ys.
+move=> /(@sorted_lt_nth x0 (x0 :: s')).
+by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
+Qed.
+
+Hypothesis r_refl : reflexive r.
+
+Lemma sorted_le_nth x0 (s : seq T) : sorted r s ->
+  {in [pred n | n < size s] &, {homo nth x0 s : i j / i <= j >-> r i j}}.
+Proof.
+move=> s_sorted x y xs ys.
+by rewrite leq_eqVlt=> /orP[/eqP->//|/sorted_lt_nth]; apply.
+Qed.
+
+Lemma leq_index (s : seq T) : sorted r s ->
+  {in s &, forall x y, index x s <= index y s -> r x y}.
+Proof.
+case: s => [//|x0 s'] r_sorted x y xs ys.
+move=> /(@sorted_le_nth x0 (x0 :: s')).
+by rewrite ?nth_index ?[_ \in gtn _]index_mem //; apply.
+Qed.
+
+End Monotonicity.
\ No newline at end of file
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index a574710..a9cc2ac 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1842,6 +1842,12 @@ Proof. by rewrite -[s1 in subseq s1]cats0 cat_subseq ?sub0seq. Qed.
 Lemma suffix_subseq s1 s2 : subseq s2 (s1 ++ s2).
 Proof. exact: cat_subseq (sub0seq s1) _. Qed.
 
+Lemma take_subseq s i : subseq (take i s) s.
+Proof. by rewrite -[s in X in subseq _ X](cat_take_drop i) prefix_subseq. Qed.
+
+Lemma drop_subseq s i : subseq (drop i s) s.
+Proof. by rewrite -[s in X in subseq _ X](cat_take_drop i) suffix_subseq. Qed.
+
 Lemma mem_subseq s1 s2 : subseq s1 s2 -> {subset s1 <= s2}.
 Proof. by case/subseqP=> m _ -> x; apply: mem_mask. Qed.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 581a7ee..c2bd9f7 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -361,6 +361,12 @@ Proof. by rewrite eqn_leq (leqNgt n) => ->. Qed.
 Lemma ltn_eqF m n : m < n -> m == n = false.
 Proof. by move/gtn_eqF; rewrite eq_sym. Qed.
 
+Lemma ltn_geF m n : m < n -> m >= n = false.
+Proof. by rewrite (leqNgt n) => ->. Qed.
+
+Lemma leq_gtF m n : m <= n -> m > n = false.
+Proof. by rewrite (ltnNge n) => ->. Qed.
+
 Lemma leq_eqVlt m n : (m <= n) = (m == n) || (m < n).
 Proof. by elim: m n => [|m IHm] []. Qed.
 
@@ -1375,6 +1381,138 @@ rewrite -[4]/(2 * 2) -mulnA mul2n -addnn sqrnD; apply/leqifP.
 by rewrite ltn_add2r eqn_add2r ltn_neqAle !nat_Cauchy; case: ifP => ->.
 Qed.
 
+Section Monotonicity.
+Variable T : Type.
+
+Lemma homo_ltn_in (D : pred nat) (f : nat -> T) (r : T -> T -> Prop) :
+  (forall y x z, r x y -> r y z -> r x z) ->
+  {in D &, forall i j k, i < k < j -> k \in D} ->
+  {in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} ->
+  {in D &, {homo f : i j / i < j >-> r i j}}.
+Proof.
+move=> r_trans Dcx r_incr i j iD jD lt_ij; move: (lt_ij) (jD) => /subnKC<-.
+elim: (_ - _) => [|k ihk]; first by rewrite addn0 => Dsi; apply: r_incr.
+move=> DSiSk [: DSik]; apply: (r_trans _ _ _ (ihk _)); rewrite ?addnS.
+  by abstract: DSik; apply: (Dcx _ _ iD DSiSk); rewrite ltn_addr ?addnS /=.
+by apply: r_incr; rewrite -?addnS.
+Qed.
+
+Lemma homo_ltn (f : nat -> T) (r : T -> T -> Prop) :
+  (forall y x z, r x y -> r y z -> r x z) ->
+  (forall i, r (f i) (f i.+1)) -> {homo f : i j / i < j >-> r i j}.
+Proof. by move=> /(@homo_ltn_in predT f) fr fS i j; apply: fr. Qed.
+
+Lemma homo_leq_in (D : pred nat) (f : nat -> T) (r : T -> T -> Prop) :
+  (forall x, r x x) -> (forall y x z, r x y -> r y z -> r x z) ->
+  {in D &, forall i j k, i < k < j -> k \in D} ->
+  {in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} ->
+  {in D &, {homo f : i j / i <= j >-> r i j}}.
+Proof.
+move=> r_refl r_trans Dcx /(homo_ltn_in r_trans Dcx) lt_r i j iD jD.
+by rewrite leq_eqVlt => /predU1P[->//|/lt_r]; apply.
+Qed.
+
+Lemma homo_leq (f : nat -> T) (r : T -> T -> Prop) :
+   (forall x, r x x) -> (forall y x z, r x y -> r y z -> r x z) ->
+  (forall i, r (f i) (f i.+1)) -> {homo f : i j / i <= j >-> r i j}.
+Proof. by move=> rrefl /(@homo_leq_in predT f r) fr fS i j; apply: fr. Qed.
+
+Section NatToNat.
+Variable (f : nat -> nat).
+
+(****************************************************************************)
+(* This listing of "Let"s factor out the required premices for the          *)
+(* subsequent lemmas, putting them in the context so that "done" solves the *)
+(* goals quickly                                                            *)
+(****************************************************************************)
+
+Let ltn_neqAle := ltn_neqAle.
+Let gtn_neqAge x y : (y < x) = (x != y) && (y <= x).
+Proof. by rewrite ltn_neqAle eq_sym. Qed.
+Let anti_leq := anti_leq.
+Let anti_geq : antisymmetric geq.
+Proof. by move=> m n /=; rewrite andbC => /anti_leq. Qed.
+Let leq_total := leq_total.
+
+Lemma ltnW_homo : {homo f : m n / m < n} -> {homo f : m n / m <= n}.
+Proof. exact: homoW. Qed.
+
+Lemma homo_inj_lt : injective f -> {homo f : m n / m <= n} ->
+  {homo f : m n / m < n}.
+Proof. exact: inj_homo. Qed.
+
+Lemma ltnW_nhomo : {homo f : m n /~ m < n} -> {homo f : m n /~ m <= n}.
+Proof. exact: homoW. Qed.
+
+Lemma nhomo_inj_lt : injective f -> {homo f : m n /~ m <= n} ->
+  {homo f : m n /~ m < n}.
+Proof. exact: inj_homo. Qed.
+
+Lemma incrn_inj : {mono f : m n / m <= n} -> injective f.
+Proof. exact: mono_inj. Qed.
+
+Lemma decrn_inj : {mono f : m n /~ m <= n} -> injective f.
+Proof. exact: mono_inj. Qed.
+
+Lemma leqW_mono : {mono f : m n / m <= n} -> {mono f : m n / m < n}.
+Proof. exact: anti_mono. Qed.
+
+Lemma leqW_nmono : {mono f : m n /~ m <= n} -> {mono f : m n /~ m < n}.
+Proof. exact: anti_mono. Qed.
+
+Lemma leq_mono : {homo f : m n / m < n} -> {mono f : m n / m <= n}.
+Proof. exact: total_homo_mono. Qed.
+
+Lemma leq_nmono : {homo f : m n /~ m < n} -> {mono f : m n /~ m <= n}.
+Proof. exact: total_homo_mono. Qed.
+
+Variable (D D' : pred nat).
+
+Lemma ltnW_homo_in : {in D & D', {homo f : m n / m < n}} ->
+  {in D & D', {homo f : m n / m <= n}}.
+Proof. exact: homoW_in. Qed.
+
+Lemma ltnW_nhomo_in : {in D & D', {homo f : m n /~ m < n}} ->
+                 {in D & D', {homo f : m n /~ m <= n}}.
+Proof. exact: homoW_in. Qed.
+
+Lemma homo_inj_lt_in : {in D & D', injective f} ->
+                        {in D & D', {homo f : m n / m <= n}} ->
+  {in D & D', {homo f : m n / m < n}}.
+Proof. exact: inj_homo_in. Qed.
+
+Lemma nhomo_inj_lt_in : {in D & D', injective f} ->
+                        {in D & D', {homo f : m n /~ m <= n}} ->
+  {in D & D', {homo f : m n /~ m < n}}.
+Proof. exact: inj_homo_in. Qed.
+
+Lemma incrn_inj_in : {in D &, {mono f : m n / m <= n}} ->
+  {in D &, injective f}.
+Proof. exact: mono_inj_in. Qed.
+
+Lemma decrn_inj_in : {in D &, {mono f : m n /~ m <= n}} ->
+  {in D &, injective f}.
+Proof. exact: mono_inj_in. Qed.
+
+Lemma leqW_mono_in : {in D &, {mono f : m n / m <= n}} ->
+  {in D &, {mono f : m n / m < n}}.
+Proof. exact: anti_mono_in. Qed.
+
+Lemma leqW_nmono_in : {in D &, {mono f : m n /~ m <= n}} ->
+  {in D &, {mono f : m n /~ m < n}}.
+Proof. exact: anti_mono_in. Qed.
+
+Lemma leq_mono_in : {in D &, {homo f : m n / m < n}} ->
+  {in D &, {mono f : m n / m <= n}}.
+Proof. exact: total_homo_mono_in. Qed.
+
+Lemma leq_nmono_in : {in D &, {homo f : m n /~ m < n}} ->
+  {in D &, {mono f : m n /~ m <= n}}.
+Proof. exact: total_homo_mono_in. Qed.
+
+End NatToNat.
+End Monotonicity.
+
 (* Support for larger integers. The normal definitions of +, - and even  *)
 (* IO are unsuitable for Peano integers larger than 2000 or so because   *)
 (* they are not tail-recursive. We provide a workaround module, along    *)