Theorem: extraction_ge (LCTutorial/Exercises/Topics/SequenceLimits.lean)

State before:
φ : ℕ → ℕ
⊢ extraction φ → ∀ (N N' : ℕ), ∃ n ≥ N', φ n ≥ N
Tactic:
sorry
State after:
no goals