proposition: Lemma even_odd_destruct: forall n, (exists a, n = 2 * a) \/ (exists a, n = 2 * a + 1).
proof: Proof. induction n. - left. exists 0. reflexivity. - destruct IHn as [[a E] | [a E]]. + right. exists a. lia. + left. exists (S a). lia. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Bool.Bool Coq.Arith.Arith Coq.micromega.Lia Coq.NArith.NArith Coq.ZArith.ZArith bbv.N_Z_nat_conversions bbv.Nomega