proposition: Theorem strong_ind_index_seq_with_prop {Q : nat -> Prop} (H0 : {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)) -> {n_kplus1 : nat | Q n_kplus1 /\ n k < n_kplus1}) : {n : nat -> nat | is_index_seq n /\ forall k : nat, Q (n k)}.
proof: Proof. enough {n : nat -> nat | forall k : nat, index_seq_prop_family Q k n} as [n Hn]. { exists n. apply reformulate_final_prop_index. exact Hn. } destruct H0 as [n0 Hn0]. apply (strong_ind_seq_with_prop (dep_only_on_start_index_seq_prop_family Q) n0). - apply (reformulate_base_prop_index (const_seq n0)). exact Hn0. - intro k. assert (S k = k + 1) as Sk_eq_kplus1 by lia; rewrite Sk_eq_kplus1. apply reformulate_step_prop_index. apply Hstep. Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric