diff options
| author | Cyril Cohen | 2019-11-18 15:19:09 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-11-18 15:20:15 +0100 |
| commit | 359abfc1d67843216b0362d2fee3b8d650ff7ec0 (patch) | |
| tree | 088824008788e0de5aa328f18f6b7824d6503019 /mathcomp | |
| parent | f6d25edde35e9e1fe6260c7bd3a0717147560d40 (diff) | |
Documenting `L` and `R` in `CONTRIBUTING.md`
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 10 |
1 files changed, 5 insertions, 5 deletions
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. |