proposition: Lemma index_seq_grows_0 : ∀ n : ℕ → ℕ, is_index_seq n ⇒ ∀ k : ℕ, (n k ≥ k)%nat.
proof: Proof. Take n : (ℕ → ℕ); such that (is_index_seq n). induction k as [|k IH]. - We conclude that (n 0 >= 0)%nat. - It holds that (for all k0 : ℕ, (n k0 < n (S k0))%nat). It holds that (n k < n (S k))%nat. We conclude that (n (S k) ≥ S k)%nat. Qed.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove