fact: Definition is_subsequence (b : ℕ → X) (a : ℕ → X) := ∃ m : (ℕ → ℕ), is_index_sequence m ∧ ∀ k : ℕ, b k = (a ◦ m) k.
imports: Coq.Reals.Reals Automation Libs.Analysis.MetricSpaces Libs.Analysis.SequencesMetric Notations Tactics