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, 14 insertions, 14 deletions

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 7663e63..eaa256c 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.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 ssrnum ssrint rat matrix.
 From mathcomp Require Import polydiv finalg perm zmodp mxalgebra vector.
 
@@ -46,7 +46,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import GRing.Theory Num.Theory.
+Import Order.Theory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
 Definition divz (m d : int) :=
@@ -79,7 +79,7 @@ Proof. by case: d => // d; rewrite /divz /= mul1r. Qed.
 Lemma divzN m d : (m %/ - d)%Z = - (m %/ d)%Z.
 Proof. by case: m => n; rewrite /divz /= sgzN abszN mulNr. Qed.
 
-Lemma divz_abs m d : (m %/ `|d|)%Z = (-1) ^+ (d < 0)%R * (m %/ d)%Z.
+Lemma divz_abs (m d : int) : (m %/ `|d|)%Z = (-1) ^+ (d < 0)%R * (m %/ d)%Z.
 Proof.
 by rewrite {3}[d]intEsign !mulr_sign; case: ifP => -> //; rewrite divzN opprK.
 Qed.
@@ -132,7 +132,7 @@ Qed.
 
 Lemma divzMDl q m d : d != 0 -> ((q * d + m) %/ d)%Z = q + (m %/ d)%Z.
 Proof.
-rewrite neqr_lt -oppr_gt0 => nz_d.
+rewrite neq_lt -oppr_gt0 => nz_d.
 wlog{nz_d} d_gt0: q d / d > 0; last case: d => // d in d_gt0 *.
   move=> IH; case/orP: nz_d => /IH// /(_  (- q)).
   by rewrite mulrNN !divzN -opprD => /oppr_inj.
@@ -179,8 +179,8 @@ Lemma divzMpl p m d : p > 0 -> (p * m %/ (p * d) = m %/ d)%Z.
 Proof.
 case: p => // p p_gt0; wlog d_gt0: d / d > 0; last case: d => // d in d_gt0 *.
   by move=> IH; case/intP: d => [|d|d]; rewrite ?mulr0 ?divz0 ?mulrN ?divzN ?IH.
-rewrite {1}(divz_eq m d) mulrDr mulrCA divzMDl ?mulf_neq0 ?gtr_eqF // addrC.
-rewrite divz_small ?add0r // PoszM pmulr_rge0 ?modz_ge0 ?gtr_eqF //=.
+rewrite {1}(divz_eq m d) mulrDr mulrCA divzMDl ?mulf_neq0 ?gt_eqF // addrC.
+rewrite divz_small ?add0r // PoszM pmulr_rge0 ?modz_ge0 ?gt_eqF //=.
 by rewrite ltr_pmul2l ?ltz_pmod.
 Qed.
 Arguments divzMpl [p m d].
@@ -203,19 +203,20 @@ Qed.
  
 Lemma ltz_ceil m d : d > 0 -> m < ((m %/ d)%Z + 1) * d.
 Proof.
-by case: d => // d d_gt0; rewrite mulrDl mul1r -ltr_subl_addl ltz_mod ?gtr_eqF.
+by case: d => // d d_gt0; rewrite mulrDl mul1r -ltr_subl_addl ltz_mod ?gt_eqF.
 Qed.
 
 Lemma ltz_divLR m n d : d > 0 -> ((m %/ d)%Z < n) = (m < n * d).
 Proof.
 move=> d_gt0; apply/idP/idP.
-  by rewrite -lez_addr1 -(ler_pmul2r d_gt0); apply: ltr_le_trans (ltz_ceil _ _).
-rewrite -(ltr_pmul2r d_gt0 _ n) //; apply: ler_lt_trans (lez_floor _ _).
-by rewrite gtr_eqF.
+  by rewrite -[_ < n]lez_addr1 -(ler_pmul2r d_gt0);
+     apply: lt_le_trans (ltz_ceil _ _).
+rewrite -(ltr_pmul2r d_gt0 _ n) //; apply: le_lt_trans (lez_floor _ _).
+by rewrite gt_eqF.
 Qed.
 
 Lemma lez_divRL m n d : d > 0 -> (m <= (n %/ d)%Z) = (m * d <= n).
-Proof. by move=> d_gt0; rewrite !lerNgt ltz_divLR. Qed.
+Proof. by move=> d_gt0; rewrite !leNgt ltz_divLR. Qed.
 
 Lemma divz_ge0 m d : d > 0 -> ((m %/ d)%Z >= 0) = (m >= 0).
 Proof. by case: d m => // d [] n d_gt0; rewrite (divz_nat, divNz_nat). Qed.
@@ -225,9 +226,9 @@ Proof.
 case: n => // [[|n]] _; first by rewrite mul0r !divz0 div0z.
 wlog p_gt0: p / p > 0; last case: p => // p in p_gt0 *.
   by case/intP: p => [|p|p] IH; rewrite ?mulr0 ?divz0 ?mulrN ?divzN // IH.
-rewrite {2}(divz_eq m (n.+1%:Z * p)) mulrA mulrAC !divzMDl // ?gtr_eqF //.
+rewrite {2}(divz_eq m (n.+1%:Z * p)) mulrA mulrAC !divzMDl // ?gt_eqF //.
 rewrite [rhs in _ + rhs]divz_small ?addr0 // ltz_divLR // divz_ge0 //.
-by rewrite mulrC ltz_pmod ?modz_ge0 ?gtr_eqF ?pmulr_lgt0.
+by rewrite mulrC ltz_pmod ?modz_ge0 ?gt_eqF ?pmulr_lgt0.
 Qed.
 
 Lemma modz_small m d : 0 <= m < d -> (m %% d)%Z = m.
@@ -1073,4 +1074,3 @@ rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M.
   by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV.
 by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE.
 Qed.
-