diff options
| author | Cyril Cohen | 2020-08-16 20:59:11 +0200 |
|---|---|---|
| committer | GitHub | 2020-08-16 20:59:11 +0200 |
| commit | ecf208b1d15aba433f3f11cc87b17a1b48c4d8df (patch) | |
| tree | 0d8e528124a17c39e0b8e656477abf891741cd03 | |
| parent | 43ac266e1e99cad08a9c291b99efcc7eddc244e7 (diff) | |
| parent | a79d4d915f64d0eb8d2da4a0ba4d29048b94306b (diff) | |
Merge pull request #517 from thery/minn
Extra theorems about subn minn and maxn
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 14 |
2 files changed, 15 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a684cb3..8dd9383 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -20,6 +20,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `finset.v`, neq lemmas: `set_enum`, `cards_eqP`, `cards2P` - in `fingraph.v`, new lemmas: `fcard_gt0P`, `fcard_gt1P` - in `finset.v`, new lemmas: `properC`, `properCr`, `properCl` +- in `ssrnat.v`, new lemmas: `subn_minl`, `subn_maxl` ### Changed diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 6837eb1..90b1f1d 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -673,6 +673,13 @@ Proof. by move=> m1 m2 n; rewrite !maxnE subnDr addnAC. Qed. Lemma addn_maxr : right_distributive addn maxn. Proof. by move=> m n1 n2; rewrite !(addnC m) addn_maxl. Qed. +Lemma subn_maxl : left_distributive subn maxn. +Proof. +move=> m n p; apply/eqP. +rewrite eqn_leq !geq_max !leq_sub2r leq_max ?leqnn ?andbT ?orbT // /maxn. +by case: (_ < _); rewrite leqnn // orbT. +Qed. + Lemma min0n : left_zero 0 minn. Proof. by case. Qed. Lemma minn0 : right_zero 0 minn. Proof. by []. Qed. @@ -734,6 +741,13 @@ Proof. by move=> m1 m2 n; rewrite !minnE subnDl addnBA ?leq_subr. Qed. Lemma addn_minl : left_distributive addn minn. Proof. by move=> m1 m2 n; rewrite -!(addnC n) addn_minr. Qed. +Lemma subn_minl : left_distributive subn minn. +Proof. +move=> m n p; apply/eqP. +rewrite eqn_leq !leq_min !leq_sub2r geq_min ?leqnn ?orbT //= /minn. +by case: (_ < _); rewrite leqnn // orbT. +Qed. + Lemma minnSS m n : minn m.+1 n.+1 = (minn m n).+1. Proof. by rewrite -(addn_minr 1). Qed. |