---

Step * of Lemma isqrt-non-decreasing

∀[x,y:ℕ].  isqrt(x) ≤ isqrt(y) supposing x ≤ y
BY
{ TACTIC:(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))) }

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:
TACTIC:(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)))

---

Home Index