---

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
{ (CaseNat 0 `v' THEN Auto') }

---

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:
(CaseNat  0  `v'  THEN  Auto')

---

Home Index