proposition: Lemma even_induction : forall P : nat -> CProp, P 0 -> (forall n, Nat.Even n -> P n -> P (S (S n))) -> forall n, Nat.Even n -> P n.
proof: Proof. intros P H0 H n; induction n as [n IH] using Wf_nat.lt_wf_rect. destruct n as [| n]. - intros _; exact H0. - destruct n as [| n]. + intros C%Nat.even_spec; discriminate C. + intros Hn; apply ->Nat.Even_succ_succ in Hn. apply H; [exact Hn |]. apply IH; [| exact Hn]. apply Nat.lt_trans with (1 := Nat.lt_succ_diag_r n). exact (Nat.lt_succ_diag_r _). Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)