---

Step * 1 2 of Lemma isqrt-convex


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

1
1. a : ℕ
2. b : ℕa
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{}
2.  b  :  \mBbbN{}a
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:
xxx(InstLemma  `isqrt-non-decreasing`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}a  -  b\mkleeneclose{}]\mcdot{}  THENA  Auto')xxx

---

Home Index