proposition: Lemma Codd_even_to : forall n : nat, (Codd n -> Nat.Odd n) /\ (Ceven n -> Nat.Even n).
proof: Proof. simple induction n. split. intro H. inversion H. intro. now exists 0. intros n0 H. elim H; intros H0 H1. split. intro H2. inversion H2. apply Nat.Odd_succ. apply H1. assumption. intro H2. inversion H2. apply Nat.Even_succ. apply H0. assumption. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)