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