proposition: Lemma quant_over_start_dep_only_on_start {A : Type} {P : nat -> (nat -> A) -> Prop} : dep_only_on_start P -> dep_only_on_start (fun (k : nat) (seq : nat -> A) => forall l : nat, l <= k -> P l seq).
proof: Proof. intros HypP k b c start_b_eq_c Hb l l_le_k. apply (HypP _ b). - intros i i_le_l. apply start_b_eq_c; lia. - apply Hb; assumption. Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric