proposition: Lemma dep_only_on_start_index_seq_prop_family (Q : nat -> Prop) : dep_only_on_start (index_seq_prop_family Q).
proof: Proof. intros k b c b_eq_c_start Hb. induction k. - simpl. assert (0 <= 0) as O_le_O by lia. rewrite <- (b_eq_c_start 0 O_le_O). exact Hb. - simpl. assert (k + 1 <= S k) as kplus1_le_Sk by lia. rewrite <- (b_eq_c_start (k + 1) kplus1_le_Sk). assert (k <= S k) as k_le_Sk by lia. rewrite <- (b_eq_c_start k k_le_Sk). exact Hb. Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric