proposition: Lemma Even_or_Odd x : Even x \/ Odd x.
proof: Proof. rewrite (div_mod_eq x 2). assert (h1: 0 <= x). lia. assert (h2: 0 < 2). lia. generalize (mod_bound_pos x 2 h1 h2). generalize (x mod 2). intro n. destruct n; intro h. left. exists (x / 2). lia. destruct n. right. exists (x / 2). reflexivity. lia. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat