proposition: Lemma index_sequence_property2 (n : ℕ → ℕ) : is_index_sequence n ⇒ ∀ k1 k2 : ℕ, (k1 ≥ k2)%nat ⇒ (n k1 ≥ n k2)%nat.
proof: Proof. Assume that (is_index_sequence n). Take k1, k2 : ℕ; such that (k1 ≥ k2)%nat. We need to show that (n k1 ≥ n k2)%nat. By incr_loc_to_glob it suffices to show that (is_increasing n). We need to show that (for all k : ℕ, (n k ≤ n (k + 1))%nat). Take k : ℕ. We conclude that (n k ≤ n (k+1))%nat. Qed.
imports: Coq.Reals.Reals Automation Libs.Analysis.MetricSpaces Libs.Analysis.SequencesMetric Notations Tactics