proposition: Theorem classic_strong_ind_index_seq_with_prop {Q : nat -> Prop} (H0 : exists n_0 : nat, Q n_0) (Hstep : forall (k : nat) (n : nat -> nat), (forall l : nat, l <= k -> Q (n l)) -> (forall l : nat, l < k -> n l < n (l + 1)) -> exists n_kplus1 : nat, Q n_kplus1 /\ n k < n_kplus1) : exists n : nat -> nat, is_index_seq n /\ forall k : nat, Q (n k).
proof: Proof. destruct H0 as [n0 Hn0]. assert {n0 | Q n0} as H0sig by (exists n0; exact Hn0). pose (help_with_choice Hstep) as Hstep2. destruct Hstep2 as [f Hf]. enough {n : nat -> nat | is_index_seq n /\ (forall k : nat, Q (n k))} as [n Hn]. { exists n; exact Hn. } apply (strong_ind_index_seq_with_prop H0sig). intros k n H1 H2. exists (f k n H1 H2). apply Hf. Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric