proposition: Lemma not_Even_is_Odd x : (~Even x) = Odd x.
proof: Proof. apply prop_ext; intro h; generalize (Even_or_Odd x); intros [i|i]. apply False_rec. exact (h i). exact i. destruct h as [k hk]. destruct i as [l hl]. lia. intros [k hk]. destruct i as [l hl]. lia. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat