diff options
| -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 6cf8090..df38efa 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. |