---

Step * 2 1 of Lemma integer-sqrt-newton


1. x : ℕ@i
2. ¬(x = 0 ∈ ℤ)
⊢ x < (x + 1) * (x + 1)
BY
{ TACTIC:((InstLemma `square_non_neg` [⌜x⌝]⋅ THENA Auto) THEN RW IntNormC 0⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}@i
2.  \mneg{}(x  =  0)
\mvdash{}  x  <  (x  +  1)  *  (x  +  1)


By

---

Latex:
TACTIC:((InstLemma  `square\_non\_neg`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RW  IntNormC  0\mcdot{}  THEN  Auto')

---

Home Index