proposition: Lemma index_sequence_property (n : ℕ → ℕ) : is_index_sequence n ⇒ ∀ k : ℕ, (n k ≥ k)%nat.
proof: Proof. intros. unfold is_index_sequence in H. induction k. specialize (H 0%nat). unfold ge. apply Nat.le_0_l. specialize (H k). unfold ge. apply Nat.le_succ_l. rewrite Nat.add_1_r in H. apply (Nat.le_lt_trans k (n k)). apply IHk. apply H. Qed.
imports: Coq.Reals.Reals Automation Libs.Analysis.MetricSpaces Libs.Analysis.SequencesMetric Notations Tactics