proposition: Lemma Ceven_to : forall n : nat, Ceven n -> Nat.Even n.
proof: Proof. intros n H. elim (Codd_even_to n); auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)