Theorem: exercise2_7 (LeanCourse/Assignments/Assignment2.lean)

State before:
s t : ℕ → ℕ
k : ℕ
⊢ ∃ s, EventuallyGrowsFaster (fun n => s (n + 1)) s ∧ ∀ (n : ℕ), s n ≠ 0
Tactic:
sorry
State after:
no goals