From f6d25edde35e9e1fe6260c7bd3a0717147560d40 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 25 Oct 2019 20:26:26 +0200 Subject: More arithmetic theorems - Generalizing `ltn_subr` - Adding `ltn_subl` and `ltn_subr` - Changing conclusion of `ltn_predl` to `0 < n` instead of `n != 0` --- mathcomp/ssreflect/ssrnat.v | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'mathcomp') 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. -- cgit v1.2.3 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 From 95e69d88e9f629c043939b8315e73dbb58852d9a Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 18 Nov 2019 15:39:33 +0100 Subject: fixing CHANGELOG and ltn_pred lemmas --- mathcomp/ssreflect/ssrnat.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 6e54a55..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) = (0 < n). +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. -- cgit v1.2.3