---

Step * 1 1 of Lemma tsqrt_wf


1. n : ℕ
2. v : ℕ
3. isqrt(2 * n) = v ∈ ℕ
4. 2 * n < (v * v) + v
⊢ v - 1 ∈ ℕ
BY
{ xxx(CaseNat 0 `v' THEN Auto')xxx }

1
1. n : ℕ
2. v : ℕ
3. isqrt(2 * n) = v ∈ ℕ
4. 2 * n < (v * v) + v
5. v = 0 ∈ ℤ
⊢ 0 - 1 ∈ ℕ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  v  :  \mBbbN{}
3.  isqrt(2  *  n)  =  v
4.  2  *  n  <  (v  *  v)  +  v
\mvdash{}  v  -  1  \mmember{}  \mBbbN{}


By

---

Latex:
xxx(CaseNat  0  `v'  THEN  Auto')xxx

---

Home Index