diff options
| author | Cyril Cohen | 2020-08-25 14:51:41 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-08-25 14:51:41 +0200 |
| commit | d56db9d3a6c098055ebea57557c1d1aaf6f0c9b6 (patch) | |
| tree | 071fe357ba5d244623f8372f0573c7e3efbb1d81 /mathcomp | |
| parent | 24b1070f8aa8b3fec997380313c9387309644181 (diff) | |
Adding lemma `oddS`
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 2 |
1 files changed, 2 insertions, 0 deletions
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. |