proposition: Lemma reformulate_final_prop_index {Q : nat -> Prop} {n : nat -> nat} : (forall k : nat, index_seq_prop_family Q k n) -> is_index_seq n /\ forall k : nat, Q (n k).
proof: Proof. intro H. split. - intro k. exact (proj2 (H (S k))). - induction k. + exact (H O). + assert (S k = k + 1) as Sk_eq_kplus1 by lia; rewrite Sk_eq_kplus1. exact (proj1 (H (S k))). Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric