More arithmetic theorems

- Generalizing `ltn_subr`
- Adding `ltn_subl` and `ltn_subr`
- Changing conclusion of `ltn_predl` to `0 < n` instead of `n != 0`

2 files changed, 13 insertions, 5 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9a14eec..69f53ea 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -37,7 +37,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - Arithmetic theorems in ssrnat and div:
   - some trivial results in ssrnat: `ltn_predl`, `ltn_predr`,
-    `ltn_subr` and `predn_sub`,
+    `ltn_subr`, `leq_subl`, `ltn_subl` 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
@@ -119,6 +119,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
     `ssrnat.mc_1_9` module. One may compile proofs compatible with the version
     1.9 in newer versions by using this module.
 
+- `leq_subr` has been renamed `leq_subl` (and the latter has been reallocated)
+
 ### Removed
 
 - `fin_inj_bij` lemma is removed as a duplicate of `injF_bij` lemma
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index f358f7b..434479d 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -326,7 +326,7 @@ 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).
@@ -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_subl m n : n < n - m = false.
+Proof. by rewrite ltnNge leq_subr. Qed.
+
+Lemma leq_subl m n : n <= n - m = (m == 0) || (n == 0).
+Proof. by case: m n => [|m] [|n]; rewrite ?subn0 ?leqnn ?ltn_subl. Qed.
+
+Lemma ltn_subr m n : n - m < n = (0 < m) && (0 < n).
+Proof. by rewrite ltnNge leq_subl 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.