lim n→∞.(r(2)/r(n + 2)) = r0
{ (D 0 THEN Auto) }
1. k : ℕ+@i
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) 
 (|(r(2)/r(n + 2)) - r0| ≤ (r1/r(k)))))]