proposition: Lemma incr_loc_to_glob : ∀ g : ℕ → ℕ, is_increasing g ⇒ (∀ k l : ℕ, (k ≤ l)%nat ⇒ (g k ≤ g l)%nat).
proof: Proof. Take g : (ℕ → ℕ). We need to show that ((for all k : ℕ, (g k ≤ g (k + 1))%nat) ⇨ for all k l : ℕ, (k ≤ l ⇨ g k ≤ g l)%nat ). Assume that (∀ k : ℕ, (g k) ≤ (g (k + 1)))%nat. Take k : ℕ. We use induction on l. - We first show the base case ((k ≤ 0)%nat ⇨ (g k ≤ g 0)%nat). Assume that (k ≤ 0)%nat. It holds that (k = 0)%nat. It suffices to show that (g k = g 0)%nat. We conclude that (g k = g 0)%nat. - We now show the induction step. Assume that ((k ≤ l) ⇨ (g k ≤ g l))%nat (IH). Assume that (k ≤ l + 1)%nat. destruct (lt_eq_lt_dec k (l + 1)) as [[k_lt_Sl | k_eq_Sl] | k_gt_Sl]. + It holds that (k ≤ l)%nat. We conclude that (& g k <= g l <= g (l + 1))%nat. + It suffices to show that (g k = g (l + 1))%nat. We conclude that (g k = g (l + 1))%nat. + It holds that (¬(l + 1 < k)%nat). Contradiction. Qed.
imports: Coq.Reals.Reals Automation Libs.Analysis.MetricSpaces Libs.Analysis.SequencesMetric Notations Tactics