diff options
| author | Cyril Cohen | 2020-08-28 16:17:07 +0200 |
|---|---|---|
| committer | GitHub | 2020-08-28 16:17:07 +0200 |
| commit | 1d48732459725993cf26b88c4b4f7aad6dd8a2be (patch) | |
| tree | 5966ca239532ceb15e3436f0c49ae23ced61ccf2 | |
| parent | e725070f9809a7d63f063a359dd7ef6bd3800dfd (diff) | |
| parent | d56db9d3a6c098055ebea57557c1d1aaf6f0c9b6 (diff) | |
Merge pull request #556 from CohenCyril/oddS
Adding lemma `oddS`
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 07f4a85..138d3db 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -21,6 +21,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - 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` +- in `ssrnat.v`, new lemma: `oddS` + - Added a factory `distrLatticePOrderMixin` in order.v to build a `distrLatticeType` from a `porderType`. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 90b1f1d..8b4d39f 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -1252,6 +1252,8 @@ Proof. by rewrite mulnC mulnbl. Qed. Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false. +Lemma oddS n : odd n.+1 = ~~ odd n. Proof. by []. Qed. + Lemma oddb (b : bool) : odd b = b. Proof. by case: b. Qed. Lemma oddD m n : odd (m + n) = odd m (+) odd n. |