No Annotations
∀[x,y:ℝ]. Stable{x = y}
{ ((Unfold `req` 0 THEN Auto) THEN D 0 THEN Auto THEN SupposeNot THEN Auto) }
1. x : ℝ
2. y : ℝ
3. ¬¬(∀n:ℕ+. (|(x n) - y n| ≤ 4))
4. n : ℕ+@i
5. ¬(|(x n) - y n| ≤ 4)
⊢ |(x n) - y n| ≤ 4