---

Step * 1 2 1 of Lemma isqrt-convex


1. a : ℕ@i
2. b : ℕa@i
3. isqrt(b) ≤ isqrt(a)
4. ¬((isqrt(b) + 2) ≤ isqrt(a))
5. isqrt(1) ≤ isqrt(a - b)
⊢ (isqrt(a) - isqrt(b)) ≤ isqrt(a - b)
BY
{ TACTIC:RW (AddrC [1] (ComputeToC [])) (-1) }

1
1. a : ℕ@i
2. b : ℕa@i
3. isqrt(b) ≤ isqrt(a)
4. ¬((isqrt(b) + 2) ≤ isqrt(a))
5. 1 ≤ isqrt(a - b)
⊢ (isqrt(a) - isqrt(b)) ≤ isqrt(a - b)

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}@i
2.  b  :  \mBbbN{}a@i
3.  isqrt(b)  \mleq{}  isqrt(a)
4.  \mneg{}((isqrt(b)  +  2)  \mleq{}  isqrt(a))
5.  isqrt(1)  \mleq{}  isqrt(a  -  b)
\mvdash{}  (isqrt(a)  -  isqrt(b))  \mleq{}  isqrt(a  -  b)


By

---

Latex:
TACTIC:RW  (AddrC  [1]  (ComputeToC  []))  (-1)

---

Home Index