proposition: Lemma odd_double_ind : forall P : nat -> CProp, (forall n, Nat.Odd n -> P n) -> (forall n, 0 < n -> P n -> P (Nat.double n)) -> forall n, 0 < n -> P n.
proof: Proof. assert (forall n : nat, 0 < Nat.double n -> 0 < n) as H. { unfold Nat.double; intros [| n]; simpl; [intros []%Nat.lt_irrefl |]. intros _; exact (Nat.lt_0_succ _). } intro. intro H0. intro H1. intro n. pattern n in |- *. apply lt_wf_rect. intros n0 H2 H3. pose proof (even_or_odd_plus n0) as [k [Hk | Hk]]. - assert (0 < k) as I. { apply H; unfold Nat.double; rewrite <-Hk; exact H3. } rewrite Hk; apply H1; [exact I |]. apply H2. lia. exact I. - apply H0. exists k. lia. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)