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 (S k))%nat) ⇨ for all k l : ℕ, (k ≤ l)%nat ⇨ (g k ≤ g l)%nat). Assume that (∀ k : ℕ, (g k ≤ g (S k))%nat). Take k : ℕ. induction l as [|l IH_l]. Assume that (k ≤ 0)%nat. It holds that (k = 0)%nat. We conclude that (& g k = g 0 <= g 0)%nat. Assume that (k ≤ S l)%nat. destruct (lt_eq_lt_dec k (S l)) as [temp | k_gt_Sl]. destruct temp as [k_lt_Sl | k_eq_Sl]. It holds that (k ≤ l)%nat. By IH_l it holds that (g k ≤ g l)%nat. It holds that (g l ≤ g (S l))%nat. We conclude that (g k <= g (S l))%nat. We conclude that (& g k = g (S l) <= g (S l))%nat. It holds that (¬(S l < k)%nat). Contradiction. Qed.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove