proposition: Lemma Odd_S x : Odd (S x) = Even x.
proof: Proof. apply prop_ext; intros [k hk]. rewrite <- not_Odd_is_Even. intros [l hl]. lia. rewrite <- not_Even_is_Odd. intros [l hl]. lia. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat