Merge pull request #399 from CohenCyril/ltn_sub

More arithmetic theorems

3 files changed, 28 insertions, 17 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index e22b5c0..ca04b22 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -37,8 +37,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   `big_enum_val`, `big_enum_rank`, `big_set`.
 
 - Arithmetic theorems in ssrnat and div:
-  - some trivial results in ssrnat: `ltn_predl`, `ltn_predr`,
-    `ltn_subr` and `predn_sub`,
+  - some trivial results in ssrnat: `ltn_predL`, `ltn_predRL`,
+    `ltn_subrR`, `leq_subrR`, `ltn_subrL` and `predn_sub`,
   - theorems about `n <=/< p +/- m` and `m +/- n <=/< p`:
     `leq_psubRL`, `ltn_psubLR`, `leq_subRL`, `ltn_subLR`, `leq_subCl`,
     `leq_psubCr`, `leq_subCr`, `ltn_subCr`, `ltn_psubCl` and
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index e40c347..85ee5a9 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -96,25 +96,30 @@ Abbreviations are in the header of the file which introduces them. We list here
   - `AC` -- right commutativity.
   - `ACA` -- self-interchange (inner commutativity), e.g., `orbACA : (a || b) || (c || d) = (a || c) || (b || d).`
   - `b` -- a boolean argument, as in `andbb : idempotent andb.`
-  - `C` -- commutativity, as in `andbC : commutative andb`,
+  - `C` -- commutativity, as in `andbC : commutative andb.`
         -- alternatively, predicate or set complement, as in `predC.`
   - `CA` -- left commutativity.
   - `D` -- predicate or set difference, as in `predD.`
-  - `E` -- elimination lemma, as in `negbFE : ~~ b = false -> b`.
+  - `E` -- elimination lemma, as in `negbFE : ~~ b = false -> b.`
   - `F` or `f` -- boolean false, as in `andbF : b && false = false.`
-  - `g` -- a group argument
-  - `I` -- left/right injectivity, as in `addbI : right_injective addb` 
+  - `F` -- alternatively, about a finite type.
+  - `g` -- a group argument.
+  - `I` -- left/right injectivity, as in `addbI : right_injective addb.`
         -- alternatively predicate or set intersection, as in `predI.`
-  - `l` -- a left-hand operation, as `andb_orl : left_distributive andb orb.`
+  - `l` -- the left-hand of an operation, as in `andb_orl : left_distributive andb orb.`
+  - `L` -- the left-hand of a relation, as in `ltn_subrL : n - m < n = (0 < m) && (0 < n).`
+  - `LR` -- moving an operator from the left-hand to the right-hand of an relation, as in `leq_subLR : (m - n <= p) = (m <= n + p).`
   - `N` or `n` -- boolean negation, as in `andbN : a && (~~ a) = false.`
-  - `n` -- alternatively, it is a natural number argument,
+  - `n` -- alternatively, it is a natural number argument.
   - `N` -- alternatively ring negation, as in `mulNr : (- x) * y = - (x * y).`
   - `P` -- a characteristic property, often a reflection lemma, as in
      `andP : reflect (a /\ b) (a && b)`.
   - `r` -- a right-hand operation, as `orb_andr : right_distributive orb andb.`
-      -- alternatively, it is a ring argument
+      -- alternatively, it is a ring argument.
+  - `R` -- the right-hand of a relation, as in `ltn_subrR : n < n - m = false`.
+  - `RL` -- moving an operator from the right-hand to the left-hand of an relation, as in `ltn_subRL : (n < p - m) = (m + n < p).`
   - `T` or `t` -- boolean truth, as in `andbT: right_id true andb.`
-        -- alternatively, total set
+  - `T` -- alternatively, total set.
   - `U` -- predicate or set union, as in `predU`.
   - `W` -- weakening, as in `in1W : {in D, forall x, P} -> forall x, P.`
   - `0` -- ring or nat 0, or empty set, as in `addr0 : x + 0 = x.`
@@ -126,11 +131,11 @@ Abbreviations are in the header of the file which introduces them. We list here
   - `V` -- multiplicative inverse, as in `mulVr : x^-1 * x = 1.`
   - `X` -- exponentiation, as in `rmorphX : f (x ^+ n) = f x ^+ n.`
   - `Z` -- (left) module scaling, as in `linearZ : f (a *: v)  = s *: f v.`
-  - `z` -- an int argument
+  - `z` -- an int argument.
 #### Typical search pattern
 `Search _ "prefix" "suffix"* (symbol|pattern)* in library.`
 
-### Naming conventions for definitions (non exhaustive)	
+### Naming conventions for definitions (non exhaustive)
 
 - Structure for types
   - Mixed case, the first letter lowercase and the first letter of each internal word capitalized, end with `Type`
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index f358f7b..d47a3ba 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -326,10 +326,10 @@ Hint Resolve leqnSn : core.
 Lemma leq_pred n : n.-1 <= n.           Proof. by case: n => /=. Qed.
 Lemma leqSpred n : n <= n.-1.+1.        Proof. by case: n => /=. Qed.
 
-Lemma ltn_predl n : (n.-1 < n) = (n != 0).
+Lemma ltn_predL n : (n.-1 < n) = (0 < n).
 Proof. by case: n => [//|n]; rewrite ltnSn. Qed.
 
-Lemma ltn_predr m n : (m < n.-1) = (m.+1 < n).
+Lemma ltn_predRL m n : (m < n.-1) = (m.+1 < n).
 Proof. by case: n => [//|n]; rewrite succnK. Qed.
 
 Lemma ltn_predK m n : m < n -> n.-1.+1 = n.
@@ -517,6 +517,15 @@ Proof. by rewrite -subn_eq0 -subnDA. Qed.
 Lemma leq_subr m n : n - m <= n.
 Proof. by rewrite leq_subLR leq_addl. Qed.
 
+Lemma ltn_subrR m n : (n < n - m) = false.
+Proof. by rewrite ltnNge leq_subr. Qed.
+
+Lemma leq_subrR m n : (n <= n - m) = (m == 0) || (n == 0).
+Proof. by case: m n => [|m] [|n]; rewrite ?subn0 ?leqnn ?ltn_subrR. Qed.
+
+Lemma ltn_subrL m n : (n - m < n) = (0 < m) && (0 < n).
+Proof. by rewrite ltnNge leq_subrR negb_or !lt0n. Qed.
+
 Lemma subnKC m n : m <= n -> m + (n - m) = n.
 Proof. by elim: m n => [|m IHm] [|n] // /(IHm n) {2}<-. Qed.
 
@@ -538,9 +547,6 @@ Proof. by move=> le_pm le_pn; rewrite addnBA // addnBAC. Qed.
 Lemma subnBA m n p : p <= n -> m - (n - p) = m + p - n.
 Proof. by move=> le_pn; rewrite -{2}(subnK le_pn) subnDr. Qed.
 
-Lemma ltn_subr m n : m <= n -> (n - m < n) = (m > 0).
-Proof. by move=> le_mn; rewrite -subn_gt0 subnBA// addKn. Qed.
-
 Lemma subKn m n : m <= n -> n - (n - m) = m.
 Proof. by move/subnBA->; rewrite addKn. Qed.