proposition: Lemma even_ind : forall P : nat -> Prop, P 0 -> (forall n, Nat.Even n -> P n -> P (S (S n))) -> forall n, Nat.Even n -> P n.
proof: Proof. now intros P; apply even_induction. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)