Rename `totalLatticeMixin` to `totalPOrderMixin` and several refactor

- Rename `totalLatticeMixin` to `totalPOrderMixin`.
- Refactor num mixins.
- Use `Num.min` and `Num.max` rather than lattice notations if applicable.

4 files changed, 66 insertions, 155 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index b366d39..3a94cf1 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -145,7 +145,7 @@ coq-dev:
     - make install
   except:
     - /^experiment\/order$/
-    - /^pr-(270|383)$/
+    - /^pr-(270|388|389)$/
 
 ci-fourcolor-8.7:
   extends: .ci-fourcolor
@@ -182,7 +182,7 @@ ci-fourcolor-dev:
     - make install
   only:
     - /^experiment\/order$/
-    - /^pr-(270|383)$/
+    - /^pr-(270|388|389)$/
 
 ci-fourcolor-8.7-270:
   extends: .ci-fourcolor-270
@@ -210,7 +210,7 @@ ci-fourcolor-dev-270:
     - make install
   except:
     - /^experiment\/order$/
-    - /^pr-(270|383)$/
+    - /^pr-(270|388|389)$/
 
 ci-odd-order-8.7:
   extends: .ci-odd-order
@@ -247,7 +247,7 @@ ci-odd-order-dev:
     - make install
   only:
     - /^experiment\/order$/
-    - /^pr-(270|383)$/
+    - /^pr-(270|388|389)$/
 
 ci-odd-order-8.7-270:
  extends: .ci-odd-order-270
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 2906412..c3b7000 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1262,7 +1262,7 @@ Canonical real_divringPred := DivringPred real_divr_closed.
 End NumDomain.
 
 Lemma num_real (R : realDomainType) (x : R) : x \is real.
-Proof. by rewrite unfold_in; apply: le_total. Qed.
+Proof. exact: le_total. Qed.
 
 Fact archi_bound_subproof (R : archiFieldType) : archimedean_axiom R.
 Proof. by case: R => ? []. Qed.
@@ -1734,7 +1734,7 @@ Lemma real_wlog_ler P :
   forall a b : R, a \is real -> b \is real -> P a b.
 Proof.
 move=> sP hP a b ha hb; wlog: a b ha hb / a <= b => [hwlog|]; last exact: hP.
-by case: (real_leP ha hb)=> [/hP //|/ltW hba]; apply: sP; apply: hP.
+by case: (real_leP ha hb)=> [/hP //|/ltW hba]; apply/sP/hP.
 Qed.
 
 Lemma real_wlog_ltr P :
@@ -1743,7 +1743,7 @@ Lemma real_wlog_ltr P :
   forall a b : R, a \is real -> b \is real -> P a b.
 Proof.
 move=> rP sP hP; apply: real_wlog_ler=> // a b.
-by rewrite le_eqVlt; case: (altP (_ =P _))=> [->|] //= _ lab; apply: hP.
+rewrite le_eqVlt; case: eqVneq => [->|] //= _ lab; exact: hP.
 Qed.
 
 (* Monotony of addition *)
@@ -3042,7 +3042,7 @@ Lemma leif_pmul x1 x2 y1 y2 C1 C2 :
     0 <= x1 -> 0 <= x2 -> x1 <= y1 ?= iff C1 -> x2 <= y2 ?= iff C2 ->
   x1 * x2 <= y1 * y2 ?= iff (y1 * y2 == 0) || C1 && C2.
 Proof.
-move=> x1_ge0 x2_ge0 le_xy1 le_xy2; have [y_0 | ] := altP (_ =P 0).
+move=> x1_ge0 x2_ge0 le_xy1 le_xy2; have [y_0 | ] := eqVneq _ 0.
   apply/leifP; rewrite y_0 /= mulf_eq0 !eq_le x1_ge0 x2_ge0 !andbT.
   move/eqP: y_0; rewrite mulf_eq0.
   by case/pred2P=> <-; rewrite (le_xy1, le_xy2) ?orbT.
@@ -3811,7 +3811,7 @@ Variable p : {poly R}.
 
 Lemma poly_itv_bound a b : {ub | forall x, a <= x <= b -> `|p.[x]| <= ub}.
 Proof.
-have [ub le_p_ub] := poly_disk_bound p (`|a| `|` `|b|).
+have [ub le_p_ub] := poly_disk_bound p (Num.max `|a| `|b|).
 exists ub => x /andP[le_a_x le_x_b]; rewrite le_p_ub // lexU !ler_normr.
 by have [_|_] := ler0P x; rewrite ?ler_opp2 ?le_a_x ?le_x_b orbT.
 Qed.
@@ -4060,7 +4060,7 @@ Proof. by rewrite -normCK exprn_ge0. Qed.
 
 Lemma mul_conjC_gt0 x : (0 < x * x^*) = (x != 0).
 Proof.
-have [->|x_neq0] := altP eqP; first by rewrite rmorph0 mulr0.
+have [->|x_neq0] := eqVneq; first by rewrite rmorph0 mulr0.
 by rewrite -normCK exprn_gt0 ?normr_gt0.
 Qed.
 
@@ -4560,7 +4560,7 @@ Lemma normC_add_eq x y :
 Proof.
 move=> lin_xy; apply: sig2_eqW; pose u z := if z == 0 then 1 else z / `|z|.
 have uE z: (`|u z| = 1) * (`|z| * u z = z).
-  rewrite /u; have [->|nz_z] := altP eqP; first by rewrite normr0 normr1 mul0r.
+  rewrite /u; have [->|nz_z] := eqVneq; first by rewrite normr0 normr1 mul0r.
   by rewrite normf_div normr_id mulrCA divff ?mulr1 ?normr_eq0.
 have [->|nz_x] := eqVneq x 0; first by exists (u y); rewrite uE ?normr0 ?mul0r.
 exists (u x); rewrite uE // /u (negPf nz_x); congr (_ , _).
@@ -4573,7 +4573,7 @@ have def_xy: x * y^* = y * x^*.
   by rewrite mulrN mulrAC mulrA -mulrA mulrACA -!normCK mulNrn addNr.
 have{def_xy def2xy} def_yx: `|y * x| = y * x^*.
   by apply: (mulIf nz2); rewrite !mulr_natr mulrC normrM def2xy def_xy.
-rewrite -{1}(divfK nz_x y) (invC_norm x) mulrCA -{}def_yx !normrM invfM.
+rewrite -{1}(divfK nz_x y) invC_norm mulrCA -{}def_yx !normrM invfM.
 by rewrite mulrCA divfK ?normr_eq0 // mulrAC mulrA.
 Qed.
 
@@ -4714,9 +4714,7 @@ by rewrite -(eqP n2) -normM mul0r.
 Qed.
 
 Lemma le_def' x y : (x <= y) = (x == y) || (x < y).
-Proof.
-by rewrite eq_sym lt_def; case: eqP => //= ->; rewrite lerr.
-Qed.
+Proof. by rewrite lt_def; case: eqVneq => //= ->; rewrite lerr. Qed.
 
 Lemma le_trans : transitive (le m).
 by move=> y x z; rewrite !le_def' => /predU1P [->|hxy] // /predU1P [<-|hyz];
@@ -4768,6 +4766,7 @@ Coercion numDomainMixin : numMixin >-> mixin_of.
 End Exports.
 
 End NumMixin.
+Import NumMixin.Exports.
 
 Module RealMixin.
 Section RealMixin.
@@ -4775,7 +4774,7 @@ Variables (R : numDomainType).
 
 Variable (real : real_axiom R).
 
-Lemma le_total : totalLatticeMixin R.
+Lemma le_total : totalPOrderMixin R.
 Proof.
 move=> x y; move: (real (x - y)).
 by rewrite unfold_in !ler_def subr0 add0r opprB orbC.
@@ -4787,11 +4786,12 @@ Definition totalMixin :
 End RealMixin.
 
 Module Exports.
-Coercion le_total : real_axiom >-> totalLatticeMixin.
-Coercion totalMixin : real_axiom >-> Order.Total.mixin_of.
+Coercion le_total : real_axiom >-> totalPOrderMixin.
+Coercion totalMixin : real_axiom >-> totalOrderMixin.
 End Exports.
 
 End RealMixin.
+Import RealMixin.Exports.
 
 Module RealLeMixin.
 Section RealLeMixin.
@@ -4822,11 +4822,6 @@ Let leN_total x : 0 <= x \/ 0 <= - x.
 Proof. by apply/orP; rewrite le0N le0_total. Qed.
 
 Let le00 : 0 <= 0. Proof. by have:= le0_total m 0; rewrite orbb. Qed.
-Let le01 : 0 <= 1.
-Proof.
-by case/orP: (le0_total m 1)=> // ?; rewrite -[1]mul1r -mulrNN le0_mul ?le0N.
-Qed.
-Let lt01 : 0 < 1. Proof. by rewrite lt_def oner_eq0. Qed.
 
 Fact lt0_add x y : 0 < x -> 0 < y -> 0 < x + y.
 Proof.
@@ -4870,63 +4865,20 @@ Qed.
 Fact le_total : total (le m).
 Proof. by move=> x y; rewrite -sub_ge0 -opprB le0N orbC -sub_ge0 le0_total. Qed.
 
-Fact lerr : reflexive (le m).
-Proof. by move=> x; move: (le_total x x); rewrite orbb. Qed.
+Definition numMixin : numMixin R :=
+  NumMixin le_normD lt0_add eq0_norm (in2W le_total) normM le_def (lt_def m).
 
-Fact le_anti : antisymmetric (le m).
-Proof.
-move=> x y /andP [].
-rewrite -sub_ge0 -(sub_ge0 _ y) -opprB le0N => hxy hxy'.
-by move/eqP: (le0_anti hxy' hxy); rewrite subr_eq0 => /eqP.
-Qed.
-
-Fact le_trans : transitive (le m).
-Proof.
-by move=> x y z hyx hxz; rewrite -sub_ge0 -(subrK x z) -addrA le0_add ?sub_ge0.
-Qed.
-
-Lemma ge0_def x : (0 <= x) = (`|x| == x).
-Proof. by rewrite le_def subr0. Qed.
-
-Lemma normrMn x n : `|x *+ n| = `|x| *+ n.
-Proof.
-rewrite -mulr_natr -[RHS]mulr_natr normM.
-congr (_ * _); apply/eqP; rewrite -ge0_def.
-elim: n => [|n ih]; [exact: lerr | apply: (le_trans ih)].
-by rewrite le_def -natrB // subSnn -[_%:R]subr0 -le_def mulr1n le01.
-Qed.
-
-Lemma normrN1 : `|-1| = 1 :> R.
-Proof.
-have: `|-1| ^+ 2 == 1 :> R
-  by rewrite expr2 /= -normM mulrNN mul1r -[1]subr0 -le_def le01.
-rewrite sqrf_eq1 => /predU1P [] //; rewrite -[-1]subr0 -le_def.
-have ->: 0 <= -1 = (-1 == 0 :> R) || (0 < -1)
-  by rewrite lt_def; case: eqP => // ->.
-by rewrite oppr_eq0 oner_eq0 => /(lt0_add lt01); rewrite subrr lt_def eqxx.
-Qed.
-
-Lemma normrN x : `|- x| = `|x|.
-Proof. by rewrite -mulN1r normM -[RHS]mul1r normrN1. Qed.
-
-Definition orderMixin : leOrderMixin R :=
-  LeOrderMixin (lt_def _) (rrefl _) (rrefl _) le_anti le_trans le_total.
-
-Definition normedDomainMixin : @normed_mixin_of R R orderMixin :=
-  @Num.NormedMixin _ _ orderMixin (norm m) le_normD eq0_norm normrMn normrN.
-
-Definition numMixin : @mixin_of R orderMixin normedDomainMixin :=
-  @Num.Mixin _ orderMixin normedDomainMixin
-             lt0_add (in2W le_total) normM le_def.
+Definition orderMixin :
+  totalPOrderMixin (POrderType ring_display R numMixin) :=
+  le_total.
 
 End RealLeMixin.
 
 Module Exports.
 Notation realLeMixin := of_.
 Notation RealLeMixin := Mixin.
-Coercion orderMixin : realLeMixin >-> leOrderMixin.
-Coercion normedDomainMixin : realLeMixin >-> normed_mixin_of.
-Coercion numMixin : realLeMixin >-> mixin_of.
+Coercion numMixin : realLeMixin >-> NumMixin.of_.
+Coercion orderMixin : realLeMixin >-> totalPOrderMixin.
 End Exports.
 
 End RealLeMixin.
@@ -4959,16 +4911,11 @@ Fact lt0N x : (- x < 0) = (0 < x).
 Proof. by rewrite -sub_gt0 add0r opprK. Qed.
 Let leN_total x : 0 <= x \/ 0 <= - x.
 Proof.
-rewrite !le_def [_ == - x]eq_sym oppr_eq0 eq_sym -[0 < - x]lt0N opprK.
-apply/orP; case: (altP eqP) => //=; exact: lt0_total.
+rewrite !le_def [_ == - x]eq_sym oppr_eq0 -[0 < - x]lt0N opprK.
+apply/orP; case: (eqVneq x) => //=; exact: lt0_total.
 Qed.
 
 Let le00 : (0 <= 0). Proof. by rewrite le_def eqxx. Qed.
-Let le01 : (0 <= 1).
-Proof.
-rewrite le_def eq_sym; case: (altP eqP) => // /(lt0_total m) /orP [] //= ?.
-by rewrite -[1]mul1r -mulrNN lt0_mul -?lt0N ?opprK.
-Qed.
 
 Fact sub_ge0 x y : (0 <= y - x) = (x <= y).
 Proof. by rewrite !le_def eq_sym subr_eq0 eq_sym sub_gt0. Qed.
@@ -5019,71 +4966,30 @@ Qed.
 
 Fact lt_def x y : (x < y) = (y != x) && (x <= y).
 Proof.
-rewrite le_def eq_sym; case: eqP => //= ->; rewrite -sub_gt0 subrr.
+rewrite le_def; case: eqVneq => //= ->; rewrite -sub_gt0 subrr.
 by apply/idP=> lt00; case/negP: (lt0_ngt0 lt00).
 Qed.
 
-Fact lt_irr : irreflexive (lt m).
-Proof. by move=> x; rewrite lt_def eqxx. Qed.
-
-Fact lt_asym x y : ~~ ((x < y) && (y < x)).
-Proof.
-rewrite -[x < _]sub_gt0 -[y < _]sub_gt0 -lt0N opprB andbC.
-by apply/negP => /andP [] /lt0_ngt0; case: (_ < _).
-Qed.
-
-Fact lt_trans : transitive (lt m).
-Proof.
-move=> y x z; rewrite -sub_gt0 -![_ < z]sub_gt0.
-rewrite -[z - x](subrKA y) [_ - _ + _]addrC; exact: lt0_add.
-Qed.
-
-Lemma le_trans : transitive (le m).
-by move=> y x z; rewrite !le_def => /predU1P [->|hxy] // /predU1P [<-|hyz];
-  rewrite ?hxy ?(lt_trans hxy hyz) orbT.
-Qed.
-
-Fact lt_total x y : x != y -> (x < y) || (y < x).
-Proof.
-rewrite -subr_eq0 => /(lt0_total m).
-by rewrite -(sub_gt0 _ (x - y)) sub0r opprB !sub_gt0 orbC.
-Qed.
-
 Fact le_total : total (le m).
 Proof.
-by move=> x y; rewrite !le_def [y == x]eq_sym; case: (altP eqP) => [|/lt_total].
+move=> x y; rewrite !le_def; case: eqVneq => [->|] //=; rewrite -subr_eq0.
+by move/(lt0_total m); rewrite -(sub_gt0 _ (x - y)) sub0r opprB !sub_gt0 orbC.
 Qed.
 
-Let lt01 : 0 < 1. Proof. by rewrite lt_def oner_eq0. Qed.
-
-Lemma normrMn x n : `|x *+ n| = `|x| *+ n.
-Proof.
-rewrite -mulr_natr -[RHS]mulr_natr normM.
-congr (_ * _); apply/eqP; rewrite -[n%:R]subr0 -le_def'.
-elim: n => [|n ih]; [rewrite le_def eqxx // | apply: (le_trans ih)].
-by rewrite le_def' -natrB // subSnn -[_%:R]subr0 -le_def' mulr1n le01.
-Qed.
-
-Definition orderMixin : ltOrderMixin R :=
-  LtOrderMixin (le_def m) (rrefl _) (rrefl _)
-               lt_irr lt_trans lt_total.
-
-Definition normedDomainMixin : @normed_mixin_of R R orderMixin :=
-  @Num.NormedMixin _ _ orderMixin (norm m)
-                   le_normD eq0_norm normrMn (@normN m).
+Definition numMixin : numMixin R :=
+  NumMixin le_normD (@lt0_add m) eq0_norm (in2W le_total) normM le_def' lt_def.
 
-Definition numMixin : @mixin_of R orderMixin normedDomainMixin :=
-  @Num.Mixin _ orderMixin normedDomainMixin
-             (@lt0_add m) (in2W le_total) normM le_def'.
+Definition orderMixin :
+  totalPOrderMixin (POrderType ring_display R numMixin) :=
+  le_total.
 
 End RealLtMixin.
 
 Module Exports.
 Notation realLtMixin := of_.
 Notation RealLtMixin := Mixin.
-Coercion orderMixin : realLtMixin >-> ltOrderMixin.
-Coercion normedDomainMixin : realLtMixin >-> normed_mixin_of.
-Coercion numMixin : realLtMixin >-> mixin_of.
+Coercion numMixin : realLtMixin >-> NumMixin.of_.
+Coercion orderMixin : realLtMixin >-> totalPOrderMixin.
 End Exports.
 
 End RealLtMixin.
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 613dd91..f869378 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -161,7 +161,7 @@ have [n ub_n]: {n | forall y, root q y -> `|y| < n}.
   have /monic_Cauchy_bound[n2 ub_n2]: (-1) ^+ d *: (q \Po - 'X) \is monic.
     rewrite monicE lead_coefZ lead_coef_comp ?size_opp ?size_polyX // -/d.
     by rewrite lead_coef_opp lead_coefX (monicP mon_q) (mulrC 1) signrMK.
-  exists (n1 `|` n2) => y; rewrite ltNge ler_normr !leUx rootE.
+  exists (Num.max n1 n2) => y; rewrite ltNge ler_normr !leUx rootE.
   apply: contraL => /orP[]/andP[] => [/ub_n1/gt_eqF->// | _ /ub_n2/gt_eqF].
   by rewrite hornerZ horner_comp !hornerE opprK mulf_eq0 signr_eq0 => /= ->.
 have [p [a nz_a Dq]] := rat_poly_scale q; pose N := Num.bound `|n * a%:~R|.
@@ -505,7 +505,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
     have /(find_root r.1)[n ub_rp] := xab0; exists n.
     have [M Mgt0 ubM]: {M | 0 < M & {in Iab_ n, forall a, `|r.2.[a]| <= M}}.
       have [M ubM] := poly_itv_bound r.2 (ab_ n).1 (ab_ n).2.
-      exists (1 `|` M) => [|s /ubM vM]; first by rewrite ltxU ltr01.
+      exists (Num.max 1 M) => [|s /ubM vM]; first by rewrite ltxU ltr01.
       by rewrite lexU orbC vM.
     exists (h2 / M) => [|a xn_a]; first by rewrite divr_gt0 ?invr_gt0 ?ltr0n.
     rewrite ltr_pdivr_mulr // -(ltr_add2l h2) -mulr2n -mulr_natl divff //.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 554ae72..2d5def5 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -53,7 +53,7 @@ From mathcomp Require Import fintype tuple bigop path finset.
 (*                                                                            *)
 (* LatticeType lat_mixin == builds a distributive lattice from a porderType   *)
 (*   where lat_mixin can be of types                                          *)
-(*     latticeMixin, totalLatticeMixin, meetJoinMixin,                        *)
+(*     latticeMixin, totalPOrderMixin, meetJoinMixin,                         *)
 (*     leOrderMixin or ltOrderMixin                                           *)
 (*   or computed using IsoLatticeMixin.                                       *)
 (*                                                                            *)
@@ -103,14 +103,14 @@ From mathcomp Require Import fintype tuple bigop path finset.
 (*                   irreflexivity, transitivity and totality of lt.          *)
 (*                   (can build:  porderType, latticeType, orderType)         *)
 (*                                                                            *)
-(* - totalLatticeMixin == on a porderType T, totality of the order of T       *)
+(* - totalPOrderMixin == on a porderType T, totality of the order of T        *)
 (*                    := total (<=%O : rel T)                                 *)
 (*                   (can build: latticeType)                                 *)
 (*                                                                            *)
 (* - totalOrderMixin == on a latticeType T, totality of the order of T        *)
 (*                    := total (<=%O : rel T)                                 *)
 (*                   (can build: orderType)                                   *)
-(*    NB: this mixin is kept separate from totalLatticeMixin (even though it  *)
+(*    NB: this mixin is kept separate from totalPOrderMixin (even though it   *)
 (*        is convertible to it), in order to avoid ambiguous coercion paths.  *)
 (*                                                                            *)
 (* - latticeMixin == on a porderType T, takes meet, join                      *)
@@ -126,7 +126,7 @@ From mathcomp Require Import fintype tuple bigop path finset.
 (* - [porderMixin of T by <:] creates an porderMixin by subtyping.            *)
 (* - [totalOrderMixin of T by <:] creates the associated totalOrderMixin.     *)
 (* - PCanPOrderMixin, CanPOrderMixin create porderMixin from cancellations    *)
-(* - MonoTotalMixin creates a totalLatticeMixin from monotonicity             *)
+(* - MonoTotalMixin creates a totalPOrderMixin from monotonicity              *)
 (* - IsoLatticeMixin creates a latticeMixin from an ordered structure         *)
 (*   isomorphism (i.e. cancel f f', cancel f' f, {mono f : x y / x <= y})     *)
 (*                                                                            *)
@@ -3306,8 +3306,8 @@ End CTBLatticeTheory.
 (* FACTORIES *)
 (*************)
 
-Module TotalLatticeMixin.
-Section TotalLatticeMixin.
+Module TotalPOrderMixin.
+Section TotalPOrderMixin.
 Import POrderDef.
 Variable (disp : unit) (T : porderType disp).
 Definition of_ := total (<=%O : rel T).
@@ -3371,17 +3371,22 @@ case: (leP y z) => yz; case: (leP y x) => xy //=; first 1 last.
 Qed.
 
 Definition latticeMixin :=
-  LatticeMixin meetC joinC meetA joinA joinKI meetKU leEmeet meetUl.
+  @LatticeMixin _ (@POrder.Pack disp T (POrder.class T)) _ _
+                meetC joinC meetA joinA joinKI meetKU leEmeet meetUl.
 
-End TotalLatticeMixin.
+Definition orderMixin : totalOrderMixin (LatticeType _ latticeMixin) :=
+  m.
+
+End TotalPOrderMixin.
 
 Module Exports.
-Notation totalLatticeMixin := of_.
-Coercion latticeMixin : totalLatticeMixin >-> Order.Lattice.mixin_of.
+Notation totalPOrderMixin := of_.
+Coercion latticeMixin : totalPOrderMixin >-> Order.Lattice.mixin_of.
+Coercion orderMixin : totalPOrderMixin >-> totalOrderMixin.
 End Exports.
 
-End TotalLatticeMixin.
-Import TotalLatticeMixin.Exports.
+End TotalPOrderMixin.
+Import TotalPOrderMixin.Exports.
 
 Module LtPOrderMixin.
 Section LtPOrderMixin.
@@ -3521,7 +3526,7 @@ Let T_total_porderType : porderType tt := POrderType tt T lePOrderMixin.
 
 Let T_total_latticeType : latticeType tt :=
   LatticeType T_total_porderType
-    (le_total m : totalLatticeMixin T_total_porderType).
+    (le_total m : totalPOrderMixin T_total_porderType).
 
 Implicit Types (x y z : T_total_latticeType).
 
@@ -3597,7 +3602,7 @@ Qed.
 
 Let T_total_latticeType : latticeType tt :=
   LatticeType T_total_porderType
-   (le_total : totalLatticeMixin T_total_porderType).
+   (le_total : totalPOrderMixin T_total_porderType).
 
 Implicit Types (x y z : T_total_latticeType).
 
@@ -3658,7 +3663,7 @@ Variables (disp : unit) (T : porderType disp).
 Variables (disp' : unit) (T' : orderType disp) (f : T -> T').
 
 Lemma MonoTotal : {mono f : x y / x <= y} ->
-  totalLatticeMixin T' -> totalLatticeMixin T.
+  totalPOrderMixin T' -> totalPOrderMixin T.
 Proof. by move=> f_mono T'_tot x y; rewrite -!f_mono le_total. Qed.
 
 End Total.
@@ -3775,7 +3780,7 @@ End Partial.
 Section Total.
 Context {disp : unit} {T : orderType disp} (P : {pred T}) (sT : subType P).
 
-Definition sub_TotalOrderMixin : totalLatticeMixin (sub_POrderType sT) :=
+Definition sub_TotalOrderMixin : totalPOrderMixin (sub_POrderType sT) :=
    @MonoTotalMixin _ _ _ val (fun _ _ => erefl) (@le_total _ T).
 Canonical sub_LatticeType := Eval hnf in LatticeType sT sub_TotalOrderMixin.
 Canonical sub_OrderType := Eval hnf in OrderType sT sub_TotalOrderMixin.
@@ -3789,7 +3794,7 @@ Notation "[ 'porderMixin' 'of' T 'by' <: ]" :=
   (at level 0, format "[ 'porderMixin'  'of'  T  'by'  <: ]") : form_scope.
 
 Notation "[ 'totalOrderMixin' 'of' T 'by' <: ]" :=
-  (sub_TotalOrderMixin _ : totalLatticeMixin [porderType of T])
+  (sub_TotalOrderMixin _ : totalPOrderMixin [porderType of T])
   (at level 0, format "[ 'totalOrderMixin'  'of'  T  'by'  <: ]",
    only parsing) : form_scope.
 
@@ -4431,7 +4436,7 @@ Section Total.
 Variable (T : orderType disp1) (T' : T -> orderType disp2).
 Implicit Types (x y : {t : T & T' t}).
 
-Fact total : totalLatticeMixin [porderType of {t : T & T' t}].
+Fact total : totalPOrderMixin [porderType of {t : T & T' t}].
 Proof.
 move=> x y; rewrite !leEsig; case: (ltgtP (tag x) (tag y)) => //=.
 case: x y => [x x'] [y y']/= eqxy; elim: _ /eqxy in y' *.
@@ -4565,7 +4570,7 @@ Section Total.
 Variable (T : orderType disp1) (T' : orderType disp2).
 Implicit Types (x y : T * T').
 
-Fact total : totalLatticeMixin [porderType of T * T'].
+Fact total : totalPOrderMixin [porderType of T * T'].
 Proof.
 move=> x y; rewrite /POrderDef.le /= /le; case: (ltgtP x.1 y.1) => _ //=.
 by apply: le_total.
@@ -4940,7 +4945,7 @@ Section Total.
 Variable T : orderType disp.
 Implicit Types s : seq T.
 
-Fact total : totalLatticeMixin [porderType of seq T].
+Fact total : totalPOrderMixin [porderType of seq T].
 Proof.
 suff: total (<=%O : rel (seq T)) by [].
 by elim=> [|x1 s1 ihs1] [|x2 s2]//=; rewrite !lexi_cons; case: ltgtP => /=.
@@ -5362,7 +5367,7 @@ Section Total.
 Variables (n : nat) (T : orderType disp).
 Implicit Types (t : n.-tuple T).
 
-Definition total : totalLatticeMixin [porderType of n.-tuple T] :=
+Definition total : totalPOrderMixin [porderType of n.-tuple T] :=
    [totalOrderMixin of n.-tuple T by <:].
 Canonical latticeType := LatticeType (n.-tuple T) total.
 Canonical orderType := OrderType (n.-tuple T) total.
@@ -5526,7 +5531,7 @@ Export Order.FinCLattice.Exports.
 Export Order.Total.Exports.
 Export Order.FinTotal.Exports.
 
-Export Order.TotalLatticeMixin.Exports.
+Export Order.TotalPOrderMixin.Exports.
 Export Order.LtPOrderMixin.Exports.
 Export Order.MeetJoinMixin.Exports.
 Export Order.LeOrderMixin.Exports.