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

diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index 19871cb..efe5cea 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -568,7 +568,7 @@ End FinFieldExists.
 
 Section FinDomain.
 
-Import ssrnum ssrint algC cyclotomic Num.Theory.
+Import order ssrnum ssrint algC cyclotomic Order.Theory Num.Theory.
 Local Infix "%|" := dvdn. (* Hide polynomial divisibility. *)
 
 Variable R : finUnitRingType.
@@ -625,18 +625,18 @@ without loss n_gt1: / (1 < n)%N by rewrite ltnNge; apply: wlog_neg.
 have [q_gt0 n_gt0] := (ltnW q_gt1, ltnW n_gt1).
 have [z z_prim] := C_prim_root_exists n_gt0.
 have zn1: z ^+ n = 1 by apply: prim_expr_order.
-have /eqP-n1z: `|z| == 1.
-  by rewrite -(pexpr_eq1 n_gt0) ?normr_ge0 // -normrX zn1 normr1.
-suffices /eqP/normC_sub_eq[t n1t [Dq Dz]]: `|q%:R - z| == `|q%:R| - `|z|.
+have /eqP-n1z: `|z| == 1 by rewrite -(pexpr_eq1 n_gt0) // -normrX zn1 normr1.
+suffices /eqP/normC_sub_eq[t n1t [Dq Dz]]:
+  `|q%:R - z : algC| == `|q%:R : algC| - `|z|.
   suffices z1: z == 1 by rewrite leq_eqVlt -dvdn1 (prim_order_dvd z_prim) z1.
   by rewrite Dz n1z mul1r -(eqr_pmuln2r q_gt0) Dq normr_nat mulr_natl.
 pose aq d : algC := (cyclotomic (z ^+ (n %/ d)) d).[q%:R].
 suffices: `|aq n| <= (q - 1)%:R.
-  rewrite eqr_le ler_sub_dist andbT n1z normr_nat natrB //; apply: ler_trans.
+  rewrite eq_le ler_sub_dist andbT n1z normr_nat natrB //; apply: le_trans.
   rewrite {}/aq horner_prod divnn n_gt0 expr1 normr_prod.
   rewrite (bigD1 (Ordinal n_gt1)) ?coprime1n //= !hornerE ler_pemulr //.
   elim/big_ind: _ => // [|d _]; first exact: mulr_ege1.
-  rewrite !hornerE; apply: ler_trans (ler_sub_dist _ _).
+  rewrite !hornerE; apply: le_trans (ler_sub_dist _ _).
   by rewrite normr_nat normrX n1z expr1n ler_subr_addl (leC_nat 2).
 have Zaq d: d %| n -> aq d \in Cint.
   move/(dvdn_prim_root z_prim)=> zd_prim.