---

Step * 1 of Lemma isqrt-non-decreasing


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)
BY
{ TACTIC:((Assert y < (isqrt(y) + 1) * (isqrt(y) + 1) BY
                 (InstLemma `isqrt-property` [⌜y⌝]⋅ THEN Auto))
          THEN (Assert (isqrt(x) * isqrt(x)) ≤ x BY
                      (InstLemma `isqrt-property` [⌜x⌝]⋅ 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))
6. y < (isqrt(y) + 1) * (isqrt(y) + 1)
7. (isqrt(x) * isqrt(x)) ≤ x
⊢ isqrt(x) ≤ isqrt(y)

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}
2.  y  :  \mBbbN{}
3.  x  \mleq{}  y
4.  (isqrt(y)  +  1)  \mleq{}  isqrt(x)
5.  ((isqrt(y)  +  1)  *  (isqrt(y)  +  1))  \mleq{}  (isqrt(x)  *  isqrt(x))
\mvdash{}  isqrt(x)  \mleq{}  isqrt(y)


By

---

Latex:
TACTIC:((Assert  y  <  (isqrt(y)  +  1)  *  (isqrt(y)  +  1)  BY
                              (InstLemma  `isqrt-property`  [\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto))
                THEN  (Assert  (isqrt(x)  *  isqrt(x))  \mleq{}  x  BY
                                        (InstLemma  `isqrt-property`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto))
                )

---

Home Index