proposition: Lemma odd_induction : forall P : nat -> CProp, P 1 -> (forall n, Nat.Odd n -> P n -> P (S (S n))) -> forall n, Nat.Odd n -> P n.
proof: Proof. intros P H1 H [| n] Hn. - apply Nat.odd_spec in Hn; discriminate Hn. - apply (even_induction (fun n => P (S n))). + exact H1. + now intros k Hk; apply H, Nat.Odd_succ. + now apply Nat.Odd_succ. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)