---

Step * 1 2 of Lemma isqrt-convex


1. a : ℕ@i
2. b : ℕa@i
3. isqrt(b) ≤ isqrt(a)
4. ¬((isqrt(b) + 2) ≤ isqrt(a))
⊢ (isqrt(a) - isqrt(b)) ≤ isqrt(a - b)
BY
{ TACTIC:(InstLemma `isqrt-non-decreasing` [⌜1⌝;⌜a - b⌝]⋅ THENA Auto') }

1
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)

---

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))
\mvdash{}  (isqrt(a)  -  isqrt(b))  \mleq{}  isqrt(a  -  b)


By

---

Latex:
TACTIC:(InstLemma  `isqrt-non-decreasing`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}a  -  b\mkleeneclose{}]\mcdot{}  THENA  Auto')

---

Home Index