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

5 files changed, 368 insertions, 30 deletions

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    *)