proposition: Lemma built_seq_is_index_seq : ∀ g : ℕ → ℕ, (∀ k : ℕ, (g k ≥ k)%nat) ⇒ is_index_seq (build_seq g).
proof: Proof. Take g : (ℕ → ℕ). Assume that (for all k : ℕ, (g k ≥ k)%nat). We need to show that (for all k : ℕ, (build_seq g k < build_seq g (S k))%nat). Take k : ℕ. We need to show that (build_seq g k < g (S (seq_of_max g (build_seq g k))))%nat. It holds that (g( S(seq_of_max g (build_seq g k)))≥ S(seq_of_max g (build_seq g k)))%nat. It holds that (g( S(seq_of_max g (build_seq g k)))> seq_of_max g (build_seq g k))%nat. By elements_le_seq_of_max_pre it holds that (seq_of_max g (build_seq g k) ≥ g(build_seq g k))%nat. It holds that (g(build_seq g k) ≥ build_seq g k)%nat. We conclude that (& build_seq g k <= g(build_seq g k) <= seq_of_max g (build_seq g k) < g( S(seq_of_max g (build_seq g k))))%nat. Qed.
imports: Coq.Reals.Reals ZArith Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Negation Notations Tactics Waterprove