From d56db9d3a6c098055ebea57557c1d1aaf6f0c9b6 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 25 Aug 2020 14:51:41 +0200
Subject: Adding lemma `oddS`

---
 CHANGELOG_UNRELEASED.md     | 2 ++
 mathcomp/ssreflect/ssrnat.v | 2 ++
 2 files changed, 4 insertions(+)

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.
-- 
cgit v1.2.3