Rephrasing the doc

2 files changed, 151 insertions, 65 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 943f404..b4cc0ec 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -9,6 +9,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 ## [Unreleased]
 
 ### Added
+- Arithmetic theorems in ssrnat, div and prime about `logn`,
+    `coprime`, `gcd`, `lcm` and `partn`: `logn_coprime`, `logn_gcd`,
+    `logn_lcm`, `eq_partn_from_log` and `eqn_from_log`.
 
 - Lemmas `ltnNleqif`, `eq_leqif`, `eqTleqif` in `ssrnat`
 
@@ -115,4 +118,3 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 ### Infrastructure
 
 ### Misc
-
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 572c9ae..718eea5 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -5,7 +5,8 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 
 (******************************************************************************)
 (* This files defines types equipped with order relations.                    *)
-(* It contains several modules implementing different theories:               *)
+(*                                                                            *)
+(* Use one of the following modules implementing different theories:          *)
 (*   Order.LTheory: partially ordered types and lattices excluding complement *)
 (*                  and totality related theorems.                            *)
 (*   Order.CTheory: complemented lattices including Order.LTheory.            *)
@@ -18,45 +19,79 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (* delimiting key "O".                                                        *)
 (*                                                                            *)
 (* We provide the following structures of ordered types                       *)
-(*           porderType == the type of partially ordered types                *)
-(*     distrLatticeType == the type of distributive lattices                  *)
-(*    bDistrLatticeType == distrLatticeType with a bottom element             *)
-(*   tbDistrLatticeType == distrLatticeType with both a top and a bottom      *)
-(*   cbDistrLatticeType == the type of sectionally complemented distributive  *)
-(*                         lattices                                           *)
-(*                         (lattices with bottom and a difference operation)  *)
-(*  ctbDistrLatticeType == the type of complemented distributive lattices     *)
-(*                         (lattices with top, bottom, difference, complement)*)
-(*            orderType == the type of totally ordered types                  *)
-(*        finPOrderType == the type of partially ordered finite types         *)
-(*  finDistrLatticeType == the type of nonempty finite distributive lattices  *)
-(* finCDistrLatticeType == the type of nonempty finite complemented           *)
-(*                         distributive lattices                              *)
-(*         finOrderType == the type of nonempty totally ordered finite types  *)
+(*           porderType d == the type of partially ordered types              *)
+(*     distrLatticeType d == the type of distributive lattices                *)
+(*    bDistrLatticeType d == distrLatticeType with a bottom element           *)
+(*   tbDistrLatticeType d == distrLatticeType with both a top and a bottom    *)
+(*   cbDistrLatticeType d == the type of sectionally complemented distributive*)
+(*                           lattices                                         *)
+(*                           (lattices with bottom and a difference operation)*)
+(*  ctbDistrLatticeType d == the type of complemented distributive lattices   *)
+(*                           (lattices with top, bottom, difference,          *)
+(*                            and complement)                                 *)
+(*            orderType d == the type of totally ordered types                *)
+(*        finPOrderType d == the type of partially ordered finite types       *)
+(*  finDistrLatticeType d == the type of nonempty finite distributive lattices*)
+(* finCDistrLatticeType d == the type of nonempty finite complemented         *)
+(*                           distributive lattices                            *)
+(*         finOrderType d == the type of nonempty totally ordered finite types*)
+(*                                                                            *)
+(* Each generic partial order and lattice operations symbols also has a first *)
+(* argument which is the display, the second which is the minimal structure   *)
+(* they operate on and then the operands. Here is the exhaustive list of all  *)
+(* such symbols for partial orders and lattices together with their default   *)
+(* display (as displayed by Check). We document their meaning in the          *)
+(* paragraph adter the next.                                                  *)
+(*                                                                            *)
+(* For porderType T                                                           *)
+(*   @Order.le          disp T     == <=%O    (in fun_scope)                  *)
+(*   @Order.lt          disp T     == <%O     (in fun_scope)                  *)
+(*   @Order.comparable  disp T     == >=<%O   (in fun_scope)                  *)
+(*   @Order.ge          disp T     == >=%O    (in fun_scope)                  *)
+(*   @Order.gt          disp T     == >%O     (in fun_scope)                  *)
+(*   @Order.leif        disp T     == <?=%O   (in fun_scope)                  *)
+(* For distrLatticeType T                                                     *)
+(*   @Order.meet        disp T x y == x `&` y (in order_scope)                *)
+(*   @Order.join        disp T x y == x `|` y (in order_scope)                *)
+(* For bDistrLatticeType T                                                    *)
+(*   @Order.bottom      disp T     == 0       (in order_scope)                *)
+(* For tbDistrLatticeType T                                                   *)
+(*   @Order.top         disp T     == 1       (in order_scope)                *)
+(* For cbDistrLatticeType T                                                   *)
+(*   @Order.sub         disp T x y == x `|` y (in order_scope)                *)
+(* For ctbDistrLatticeType T                                                  *)
+(*   @Order.compl       disp T x   == ~` x    (in order_scope)                *)
 (*                                                                            *)
-(* Each of these structures take a first argument named display, of type      *)
-(* unit. Instantiating it with tt or an unknown key will lead to a default    *)
-(* display for notations, i.e. over these structures, we have:                *)
+(* This first argument named either d, disp or display, of type unit,         *)
+(* configures the printing of notations.                                      *)
+(* Instantiating d with tt or an unknown key will lead to a default           *)
+(* display for notations, i.e. we have:                                       *)
+(* For x, y of type T, where T is canonically a porderType d:                 *)
 (*            x <= y <-> x is less than or equal to y.                        *)
 (*             x < y <-> x is less than y (:= (y != x) && (x <= y)).          *)
 (*            x >= y <-> x is greater than or equal to y (:= y <= x).         *)
 (*             x > y <-> x is greater than y (:= y < x).                      *)
 (*   x <= y ?= iff C <-> x is less than y, or equal iff C is true.            *)
 (*           x >=< y <-> x and y are comparable (:= (x <= y) || (y <= x)).    *)
-(*            x >< y <-> x and y are incomparable.                            *)
-(* For lattices we provide the following operations                           *)
+(*            x >< y <-> x and y are incomparable (:= ~~ x >=< y).            *)
+(* For x, y of type T, where T is canonically a distrLatticeType d:           *)
 (*           x `&` y == the meet of x and y.                                  *)
 (*           x `|` y == the join of x and y.                                  *)
+(* In a type T, where T is canonically a bDistrLatticeType d:                 *)
 (*                 0 == the bottom element.                                   *)
+(*   \join_<range> e == iterated join of a lattice with a bottom.             *)
+(* In a type T, where T is canonically a tbDistrLatticeType d:                *)
 (*                 1 == the top element.                                      *)
+(*   \meet_<range> e == iterated meet of a lattice with a top.                *)
+(* For x, y of type T, where T is canonically a cbDistrLatticeType d:         *)
 (*           x `\` y == the (sectional) complement of y in [0, x].            *)
+(* For x of type T, where T is canonically a ctbDistrLatticeType d:           *)
 (*              ~` x == the complement of x in [0, 1].                        *)
-(*   \meet_<range> e == iterated meet of a lattice with a top.                *)
-(*   \join_<range> e == iterated join of a lattice with a bottom.             *)
 (*                                                                            *)
 (* There are three distinct uses of the symbols                               *)
-(* <, <=, >, >=, _ <= _ ?= iff _, >=<, and ><:                                *)
-(*    0-ary, unary (prefix), and binary (infix).                              *)
+(*   <, <=, >, >=, _ <= _ ?= iff _, >=<, and ><                               *)
+(*   in the default display:                                                  *)
+(* they can be 0-ary, unary (prefix), and binary (infix).                     *)
 (* 0. <%O, <=%O, >%O, >=%O, <?=%O, >=<%O, and ><%O stand respectively for     *)
 (*    lt, le, gt, ge, leif (_ <= _ ?= iff _), comparable, and incomparable.   *)
 (* 1. (< x),  (<= x), (> x), (>= x), (>=< x), and (>< x) stand respectively   *)
@@ -70,25 +105,73 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (* Alternative notation displays can be defined by :                          *)
 (* 1. declaring a new opaque definition of type unit. Using the idiom         *)
 (*    `Lemma my_display : unit. Proof. exact: tt. Qed.`                       *)
-(* 2. using this symbol to tag canoincal porderType structures using          *)
+(* 2. using this symbol to tag canonical porderType structures using          *)
 (*    `Canonical my_porderType := POrderType my_display my_type my_mixin`,    *)
 (* 3. declaring notations for the main operations of this library, by         *)
 (*    setting the first argument of the definition to the display, e.g.       *)
-(*    `Notation my_syndef_le x y := @le my_display _ x y` or                  *)
-(*    `Notation "x <<< y" := @lt my_display _ x y (at level ...)`             *)
+(*    `Notation my_syndef_le x y := @Order.le my_display _ x y.` or           *)
+(*    `Notation "x <<< y" := @Order.lt my_display _ x y (at level ...).`      *)
 (*    Non overloaded notations will default to the default display.           *)
 (*                                                                            *)
 (* One may use displays either for convenience or to desambiguate between     *)
-(* different structures defined on copies of one. Two examples of this are    *)
-(* given in this library:                                                     *)
-(* - the converse ordered structures. If T is an ordered type (and in         *)
-(*   particular porderType d), then T^c is a copy of T with the same ordered  *)
-(*   structures but with the display (converse_display d) which prints all    *)
-(*   of the above notations with an addition ^c in the notation (<=^c ...)    *)
-(* - natural number in divisibility order. The type natdvd is a copy of nat   *)
-(*   where the canonical order is given by dvdn and meet and join by gcdn     *)
-(*   and lcmn. The display is dvd_display and overloads le using %|, lt using *)
-(*   %<| and meet and join using gcd and lcm.                                 *)
+(* different structures defined on "copies" of a type (as explained below.)   *)
+(* We provide the following "copies" of types,                                *)
+(* the first one is a *documented example*                                    *)
+(*            natdvd := nat                                                   *)
+(*                   == a "copy" of nat which is canonically ordered using    *)
+(*                      divisibility predicate dvdn.                          *)
+(*                      Notation %|, %<|, gcd, lcm are used instead of        *)
+(*                      <=, <, meet and join.                                 *)
+(*              T^c  := converse T,                                           *)
+(*                      where converse is a new definition for (fun T => T)   *)
+(*                   == a "copy" of T, such that if T is canonically ordered, *)
+(*                      then T^c is canonically ordered with the converse     *)
+(*                      order, and displayed with an extra ^c in the notation *)
+(*                      i.e. <=^c, <^c, >=<^c, ><^c, `&`^c, `|`^c are         *)
+(*                      used and displayed instead of                         *)
+(*                      <=, <, >=<, ><, `&`, `|`                              *)
+(*     T *prod[d] T' := T * T'                                                *)
+(*                   == a "copy" of the cartesian product such that,          *)
+(*                      if T and T' are canonically ordered,                  *)
+(*                      then T *prod[d] T' is canonically ordered in product  *)
+(*                      order.                                                *)
+(*                      i.e. (x1, x2) <= (y1, y2) =                           *)
+(*                             (x1 <= y1) && (x2 <= y2),                      *)
+(*                      and displayed in display d                            *)
+(*           T *p T' := T *prod[prod_display] T'                              *)
+(*                      where prod_display adds an extra ^p to all notations  *)
+(*     T *lexi[d] T' := T * T'                                                *)
+(*                   == a "copy" of the cartesian product such that,          *)
+(*                      if T and T' are canonically ordered,                  *)
+(*                      then T *lexi[d] T' is canonically ordered in          *)
+(*                      lexicographic order                                   *)
+(*                      i.e. (x1, x2) <= (y1, y2) =                           *)
+(*                             (x1 <= y1) && ((x1 >= y1) ==> (x2 <= y2))      *)
+(*                      and  (x1, x2) < (y1, y2) =                            *)
+(*                             (x1 <= y1) && ((x1 >= y1) ==> (x2 < y2))       *)
+(*                      and displayed in display d                            *)
+(*           T *l T' := T *lexi[lexi_display] T'                              *)
+(*                      where lexi_display adds an extra ^l to all notations  *)
+(*  seqprod_with d T := seq T                                                 *)
+(*                   == a "copy" of seq, such that if T is canonically        *)
+(*                      ordered, then seqprod_with d T is canonically ordered *)
+(*                      in product order i.e.                                 *)
+(*                      [:: x1, .., xn] <= [y1, .., yn] =                     *)
+(*                        (x1 <= y1) && ... && (xn <= yn)                     *)
+(*                      and displayed in display d                            *)
+(* n.-tupleprod[d] T == same with n.tuple T                                   *)
+(*         seqprod T := seqprod_with prod_display T                           *)
+(*    n.-tupleprod T := n.-tuple[prod_display] T                              *)
+(*  seqlexi_with d T := seq T                                                 *)
+(*                   == a "copy" of seq, such that if T is canonically        *)
+(*                      ordered, then seqprod_with d T is canonically ordered *)
+(*                      in lexicographic order i.e.                           *)
+(*                      [:: x1, .., xn] <= [y1, .., yn] =                     *)
+(*                        (x1 <= x2) && ((x1 >= y1) ==> ((x2 <= y2) && ...))  *)
+(*                      and displayed in display d                            *)
+(* n.-tuplelexi[d] T == same with n.tuple T                                   *)
+(*         seqlexi T := lexiprod_with lexi_display T                          *)
+(*    n.-tuplelexi T := n.-tuple[lexi_display] T                              *)
 (*                                                                            *)
 (* Beware that canonical structure inference will not try to find the copy of *)
 (* the structures that fits the display one mentioned, but will rather        *)
@@ -105,7 +188,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (* The default display is tt and users can define their own as explained      *)
 (* above.                                                                     *)
 (*                                                                            *)
-(* For orderType we provide the following operations                          *)
+(* For orderType we provide the following operations (in total_display)       *)
 (*   [arg minr_(i < i0 | P) M] == a value i : T minimizing M : R, subject to  *)
 (*                      the condition P (i may appear in P and M), and        *)
 (*                      provided P holds for i0.                              *)
@@ -115,6 +198,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (*   [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.             *)
+(* with head symbols Order.arg_min and Order.arg_max                          *)
 (*                                                                            *)
 (* In order to build the above structures, one must provide the appropriate   *)
 (* mixin to the following structure constructors. The list of possible mixins *)
@@ -160,7 +244,7 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (*                                                                            *)
 (* Additionally:                                                              *)
 (* - [porderType of _] ... notations are available to recover structures on   *)
-(*    copies of the types, as in eqtype, choicetype, ssralg...                *)
+(*    "copies" of the types, as in eqtype, choicetype, ssralg...              *)
 (* - [finPOrderType of _] ... notations to compute joins between finite types *)
 (*                            and ordered types                               *)
 (*                                                                            *)
@@ -225,27 +309,27 @@ From mathcomp Require Import path fintype tuple bigop finset div prime.
 (*   are respectively gcdn and lcmn                                           *)
 (* - porderType, distrLatticeType, orderType, bDistrLatticeType,              *)
 (*   tbDistrLatticeType, cbDistrLatticeType, ctbDistrLatticeType              *)
-(*   on T *prod[disp] T' a copy of T * T'                                     *)
+(*   on T *prod[disp] T' a "copy" of T * T'                                   *)
 (*     using product order (and T *p T' its specialization to prod_display)   *)
 (* - porderType, distrLatticeType, and orderType,  on T *lexi[disp] T'        *)
-(*     another copy of T * T', with lexicographic ordering                    *)
+(*     another "copy" of T * T', with lexicographic ordering                  *)
 (*     (and T *l T' its specialization to lexi_display)                       *)
 (* - porderType, distrLatticeType, and orderType,  on {t : T & T' x}          *)
 (*     with lexicographic ordering                                            *)
 (* - porderType, distrLatticeType, orderType, bDistrLatticeType,              *)
 (*   cbDistrLatticeType, tbDistrLatticeType, ctbDistrLatticeType              *)
-(*   on seqprod_with disp T a copy of seq T                                   *)
+(*   on seqprod_with disp T a "copy" of seq T                                 *)
 (*     using product order (and seqprod T' its specialization to prod_display)*)
 (* - porderType, distrLatticeType, and orderType, on seqlexi_with disp T      *)
-(*     another copy of seq T, with lexicographic ordering                     *)
+(*     another "copy" of seq T, with lexicographic ordering                   *)
 (*     (and seqlexi T its specialization to lexi_display)                     *)
 (* - porderType, distrLatticeType, orderType, bDistrLatticeType,              *)
 (*   cbDistrLatticeType, tbDistrLatticeType, ctbDistrLatticeType              *)
-(*   on n.-tupleprod[disp] a copy of n.-tuple T                               *)
+(*   on n.-tupleprod[disp] a "copy" of n.-tuple T                             *)
 (*     using product order (and n.-tupleprod T its specialization             *)
 (*     to prod_display)                                                       *)
 (* - porderType, distrLatticeType, and orderType,  on n.-tuplelexi[d] T       *)
-(*     another copy of n.-tuple T, with lexicographic ordering                *)
+(*     another "copy" of n.-tuple T, with lexicographic ordering              *)
 (*     (and n.-tuplelexi T its specialization to lexi_display)                *)
 (* and all possible finite type instances                                     *)
 (*                                                                            *)
@@ -3972,12 +4056,12 @@ Import SubOrder.Exports.
 (* We declare two distinct canonical orders:                                  *)
 (* - leq which is total, and where meet and join are minn and maxn, on nat    *)
 (* - dvdn which is partial, and where meet and join are gcdn and lcmn,        *)
-(*   on a copy of nat we name natdiv                                          *)
+(*   on a "copy" of nat we name natdiv                                        *)
 (******************************************************************************)
 
 (******************************************************************************)
 (* The Module NatOrder defines leq as the canonical order on the type nat,    *)
-(* i.e. without creating a copy. We use the predefined total_display, which   *)
+(* i.e. without creating a "copy". We use the predefined total_display, which *)
 (* is designed to parse and print meet and join as minn and maxn. This looks  *)
 (* like standard canonical structure declaration, except we use a display.    *)
 (* We also use a single factory LeOrderMixin to instanciate three different   *)
@@ -4119,7 +4203,7 @@ End DvdSyntax.
 (* is abbreviated using the notation natdvd at the end of the module.         *)
 (* We use the newly defined dvd_display, described above. This looks          *)
 (* like standard canonical structure declaration, except we use a display and *)
-(* we declare it on a copy of the type.                                       *)
+(* we declare it on a "copy" of the type.                                     *)
 (* We first recover structures that are common to both nat and natdiv         *)
 (* (eqType, choiceType, countType) through the clone mechanisms, then we use  *)
 (* a single factory MeetJoinMixin to instanciate both porderType and          *)
@@ -4502,10 +4586,10 @@ Notation "\min^l_ ( i 'in' A ) F" :=
 
 End LexiSyntax.
 
-(***********************************************)
-(* We declare a copy of the cartesian product, *)
-(* which has canonical product order.          *)
-(***********************************************)
+(*************************************************)
+(* We declare a "copy" of the cartesian product, *)
+(* which has canonical product order.            *)
+(*************************************************)
 
 Module ProdOrder.
 Section ProdOrder.
@@ -4888,10 +4972,10 @@ End Exports.
 End SigmaOrder.
 Import SigmaOrder.Exports.
 
-(***********************************************)
-(* We declare a copy of the cartesian product, *)
-(* which has canonical lexicographic order.    *)
-(***********************************************)
+(*************************************************)
+(* We declare a "copy" of the cartesian product, *)
+(* which has canonical lexicographic order.      *)
+(*************************************************)
 
 Module ProdLexiOrder.
 Section ProdLexiOrder.
@@ -5067,10 +5151,10 @@ Canonical prodlexi_finOrderType (T : finOrderType disp1)
 End DefaultProdLexiOrder.
 End DefaultProdLexiOrder.
 
-(***************************************)
-(* We declare a copy of the sequences, *)
-(* which has canonical product order.  *)
-(***************************************)
+(*****************************************)
+(* We declare a "copy" of the sequences, *)
+(* which has canonical product order.    *)
+(*****************************************)
 
 Module SeqProdOrder.
 Section SeqProdOrder.
@@ -5240,7 +5324,7 @@ End DefaultSeqProdOrder.
 End DefaultSeqProdOrder.
 
 (*********************************************)
-(* We declare a copy of the sequences,       *)
+(* We declare a "copy" of the sequences,     *)
 (* which has canonical lexicographic order.  *)
 (*********************************************)
 
@@ -5417,7 +5501,7 @@ End DefaultSeqLexiOrder.
 End DefaultSeqLexiOrder.
 
 (***************************************)
-(* We declare a copy of the tuples,    *)
+(* We declare a "copy" of the tuples,  *)
 (* which has canonical product order.  *)
 (***************************************)
 
@@ -5698,7 +5782,7 @@ End DefaultTupleProdOrder.
 End DefaultTupleProdOrder.
 
 (*********************************************)
-(* We declare a copy of the tuples,          *)
+(* We declare a "copy" of the tuples,        *)
 (* which has canonical lexicographic order.  *)
 (*********************************************)