---

Step * 2 1 1 5 of Lemma iproper-approx


1. y : Top
2. x1 : ℕ+ ⟶ ℤ
3. [%10] : regular-seq(x1)
4. (False ∧ True) ⇒ (case ⊥ of inl(a) => a | inr(a) => a < x1)
5. n : ℕ+
6. r(-n) ≤ x1
7. (r1/r(n + 1)) < (r1/r(n))
8. r(n) < r(n + 1)
9. True ∧ True
⊢ r(-(n + 1)) < x1
BY
{ (RWO "-4<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  y  :  Top
2.  x1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  [\%10]  :  regular-seq(x1)
4.  (False  \mwedge{}  True)  {}\mRightarrow{}  (case  \mbot{}  of  inl(a)  =>  a  |  inr(a)  =>  a  <  x1)
5.  n  :  \mBbbN{}\msupplus{}
6.  r(-n)  \mleq{}  x1
7.  (r1/r(n  +  1))  <  (r1/r(n))
8.  r(n)  <  r(n  +  1)
9.  True  \mwedge{}  True
\mvdash{}  r(-(n  +  1))  <  x1


By

---

Latex:
(RWO  "-4<"  0  THEN  Auto)

---

Home Index