proposition: Lemma to_Codd : forall n : nat, Nat.Odd n -> Codd n.
proof: Proof. intros. elim (to_Codd_even n); auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)