From 359abfc1d67843216b0362d2fee3b8d650ff7ec0 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Mon, 18 Nov 2019 15:19:09 +0100
Subject: Documenting `L` and `R` in `CONTRIBUTING.md`

---
 mathcomp/ssreflect/ssrnat.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 434479d..6e54a55 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -517,14 +517,14 @@ 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.
+Lemma ltn_subrR 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 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_subr m n : n - m < n = (0 < m) && (0 < n).
-Proof. by rewrite ltnNge leq_subl negb_or !lt0n. 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.
-- 
cgit v1.2.3