proposition: Lemma reformulate_base_prop_index {Q : nat -> Prop} (n : nat -> nat) (k : nat) : Q k -> index_seq_prop_family Q 0 (const_seq k).
proof: Proof. intro Hk. simpl. unfold const_seq. exact Hk. Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric