---

Step * of Lemma isqrt-non-decreasing

∀[x,y:ℕ].  isqrt(x) ≤ isqrt(y) supposing x ≤ y
BY
{ xxx(Auto
      THEN Decide ⌜(isqrt(y) + 1) ≤ isqrt(x)⌝⋅
      THEN Auto
      THEN (Assert ((isqrt(y) + 1) * (isqrt(y) + 1)) ≤ (isqrt(x) * isqrt(x)) BY
                  (RWO "-1" 0 THEN Auto)))xxx }

1
1. x : ℕ
2. y : ℕ
3. x ≤ y
4. (isqrt(y) + 1) ≤ isqrt(x)
5. ((isqrt(y) + 1) * (isqrt(y) + 1)) ≤ (isqrt(x) * isqrt(x))
⊢ isqrt(x) ≤ isqrt(y)

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbN{}].    isqrt(x)  \mleq{}  isqrt(y)  supposing  x  \mleq{}  y


By

---

Latex:
xxx(Auto
        THEN  Decide  \mkleeneopen{}(isqrt(y)  +  1)  \mleq{}  isqrt(x)\mkleeneclose{}\mcdot{}
        THEN  Auto
        THEN  (Assert  ((isqrt(y)  +  1)  *  (isqrt(y)  +  1))  \mleq{}  (isqrt(x)  *  isqrt(x))  BY
                                (RWO  "-1"  0  THEN  Auto)))xxx

---

Home Index