src/HOL/Parity.thy

--- a/src/HOL/Parity.thy	Sun Dec 23 15:40:28 2018 +0100
+++ b/src/HOL/Parity.thy	Sun Dec 23 20:51:23 2018 +0000
@@ -549,6 +549,10 @@
   "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
   using not_mod_2_eq_1_eq_0 [of n] by simp
 
+lemma odd_card_imp_not_empty:
+  \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close>
+  using that by auto
+
 
 subsection \<open>Parity and powers\<close>