proposition: Lemma index_seq_grows : ∀ n : ℕ → ℕ, is_index_seq n ⇒ (∀ k l : ℕ, (k ≤ l)%nat ⇒ (n k - k ≤ n l - l)%nat).
proof: Proof. Take n : (ℕ → ℕ); such that (is_index_seq n). Define g := (fun (k : ℕ) ↦ (n k - k)%nat). By index_seq_strictly_incr it holds that (is_increasing g). By incr_loc_to_glob it holds that (∀ k l : ℕ, (k ≤ l)%nat ⇒ (g k ≤ g l)%nat). Take k : ℕ and l : ℕ; such that(k ≤ l)%nat. We need to show that (g k <= g l)%nat. We conclude that (g k <= g l)%nat. Qed.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove