proposition: Lemma odd_ind : forall P : nat -> Prop, P 1 -> (forall n, P n -> P (S (S n))) -> forall n, Nat.Odd n -> P n.
proof: Proof. intros P H1 H n Hn; apply odd_induction; [exact H1 | |]. - now intros k _; apply H. - exact Hn. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)