Make an appropriate use of the order library everywhere (#278, #280, #282, #283, #285, #286, #288, #296, #330, #334, and #341)

ssrnum related changes:
- Redefine the intermediate structure between `idomainType` and `numDomainType`,
  which is `normedDomainType` (normed integral domain without an order).
- Generalize (by using `normedDomainType` or the order structures), relocate
  (to order.v), and rename ssrnum related definitions and lemmas.
- Add a compatibility module `Num.mc_1_9` and export it to check compilation.
- Remove the use of the deprecated definitions and lemmas from entire theories.
- Implement factories mechanism to construct several ordered and num structures
  from fewer axioms.

order related changes:
- Reorganize the hierarchy of finite lattice structures. Finite lattices have
  top and bottom elements except for empty set. Therefore we removed finite
  lattice structures without top and bottom.
- Reorganize the theory modules in order.v:
  + `LTheory` (lattice and partial order, without complement and totality)
  + `CTheory` (`LTheory` + complement)
  + `Theory` (all)
- Give a unique head symbol for `Total.mixin_of`.
- Replace reverse and `^r` with converse and `^c` respectively.
- Fix packing and cloning functions and notations.
- Provide more ordered type instances:
  Products and lists can be ordered in two different ways: the lexicographical
  ordering and the pointwise ordering. Now their canonical instances are not
  exported to make the users choose them.
- Export `Order.*.Exports` modules by default.
- Specify the core hint database explicitly in order.v. (see #252)
- Apply 80 chars per line restriction.

General changes:
- Give consistency to shape of formulae and namings of `lt_def` and `lt_neqAle`
  like lemmas:
  lt_def    x y : (x < y) = (y != x) && (x <= y),
  lt_neqAle x y : (x < y) = (x != y) && (x <= y).
- Enable notation overloading by using scopes and displays:
  + Define `min` and `max` notations (`minr` and `maxr` for `ring_display`) as
    aliases of `meet` and `join` specialized for `total_display`.
  + Provide the `ring_display` version of `le`, `lt`, `ge`, `gt`, `leif`, and
    `comparable` notations and their explicit variants in `Num.Def`.
  + Define 3 variants of `[arg min_(i < n | P) F]` and `[arg max_(i < n | P) F]`
    notations in `nat_scope` (specialized for nat), `order_scope` (general
    version), and `ring_scope` (specialized for `ring_display`).
- Update documents and put CHANGELOG entries.

1 files changed, 11 insertions, 12 deletions

diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 3f461e3..c8ae7b1 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
-From mathcomp Require Import div choice fintype tuple finfun bigop prime.
+From mathcomp Require Import div choice fintype tuple finfun bigop prime order.
 From mathcomp Require Import ssralg poly finset fingroup morphism perm.
 From mathcomp Require Import automorphism quotient finalg action gproduct.
 From mathcomp Require Import zmodp commutator cyclic center pgroup sylow.
@@ -91,7 +91,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import GroupScope GRing.Theory Num.Theory.
+Import Order.TTheory GroupScope GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 Delimit Scope cfun_scope with CF.
 
@@ -900,7 +900,7 @@ by rewrite phi0 // => y _; apply: mul_conjC_ge0.
 Qed.
 
 Lemma cfnorm_gt0 phi : ('[phi] > 0) = (phi != 0).
-Proof. by rewrite ltr_def cfnorm_ge0 cfnorm_eq0 andbT. Qed.
+Proof. by rewrite lt_def cfnorm_ge0 cfnorm_eq0 andbT. Qed.
 
 Lemma sqrt_cfnorm_ge0 phi : 0 <= sqrtC '[phi].
 Proof. by rewrite sqrtC_ge0 cfnorm_ge0. Qed.
@@ -944,7 +944,7 @@ Lemma cfCauchySchwarz phi psi :
 Proof.
 rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC.
 have [-> | nz_psi] /= := altP (psi =P 0).
-  by apply/lerifP; rewrite !cfdot0r normCK mul0r mulr0.
+  by apply/leifP; rewrite !cfdot0r normCK mul0r mulr0.
 without loss ophi: phi / '[phi, psi] = 0.
   move=> IHo; pose a := '[phi, psi] / '[psi]; pose phi1 := phi - a *: psi.
   have ophi: '[phi1, psi] = 0.
@@ -952,7 +952,7 @@ without loss ophi: phi / '[phi, psi] = 0.
   rewrite (canRL (subrK _) (erefl phi1)) rpredDr ?rpredZ ?memv_line //.
   rewrite cfdotDl ophi add0r cfdotZl normrM (ger0_norm (cfnorm_ge0 _)).
   rewrite exprMn mulrA -cfnormZ cfnormDd; last by rewrite cfdotZr ophi mulr0.
-  by have:= IHo _ ophi; rewrite mulrDl -lerif_subLR subrr ophi normCK mul0r.
+  by have:= IHo _ ophi; rewrite mulrDl -leif_subLR subrr ophi normCK mul0r.
 rewrite ophi normCK mul0r; split; first by rewrite mulr_ge0 ?cfnorm_ge0.
 rewrite eq_sym mulf_eq0 orbC cfnorm_eq0 (negPf nz_psi) /=.
 apply/idP/idP=> [|/vlineP[a {2}->]]; last by rewrite cfdotZr ophi mulr0.
@@ -963,20 +963,19 @@ Lemma cfCauchySchwarz_sqrt phi psi :
   `|'[phi, psi]| <= sqrtC '[phi] * sqrtC '[psi] ?= iff ~~ free (phi :: psi).
 Proof.
 rewrite -(sqrCK (normr_ge0 _)) -sqrtCM ?qualifE ?cfnorm_ge0 //.
-rewrite (mono_in_lerif (@ler_sqrtC _)) 1?rpredM ?qualifE;
-rewrite ?normr_ge0 ?cfnorm_ge0 //.
+rewrite (mono_in_leif (@ler_sqrtC _)) 1?rpredM ?qualifE ?cfnorm_ge0 //.
 exact: cfCauchySchwarz.
 Qed.
 
-Lemma cf_triangle_lerif phi psi :
+Lemma cf_triangle_leif phi psi :
   sqrtC '[phi + psi] <= sqrtC '[phi] + sqrtC '[psi]
            ?= iff ~~ free (phi :: psi) && (0 <= coord [tuple psi] 0 phi).
 Proof.
-rewrite -(mono_in_lerif ler_sqr) ?rpredD ?qualifE ?sqrtC_ge0 ?cfnorm_ge0 //.
-rewrite andbC sqrrD !sqrtCK addrAC cfnormD (mono_lerif (ler_add2l _)).
+rewrite -(mono_in_leif ler_sqr) ?rpredD ?qualifE ?sqrtC_ge0 ?cfnorm_ge0 //.
+rewrite andbC sqrrD !sqrtCK addrAC cfnormD (mono_leif (ler_add2l _)).
 rewrite -mulr_natr -[_ + _](divfK (negbT (eqC_nat 2 0))) -/('Re _).
-rewrite (mono_lerif (ler_pmul2r _)) ?ltr0n //.
-have:= lerif_trans (lerif_Re_Creal '[phi, psi]) (cfCauchySchwarz_sqrt phi psi).
+rewrite (mono_leif (ler_pmul2r _)) ?ltr0n //.
+have:= leif_trans (leif_Re_Creal '[phi, psi]) (cfCauchySchwarz_sqrt phi psi).
 congr (_ <= _ ?= iff _); apply: andb_id2r.
 rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC.
 have [-> | nz_psi] := altP (psi =P 0); first by rewrite cfdot0r coord0.