---

Step * of Lemma square_non_neg

∀x:ℤ. (0 ≤ (x * x))
BY
{ ((Auto THEN InstLemma `mul_preserves_le` [⌜0⌝;⌜|x|⌝;⌜|x|⌝]⋅) THEN Auto') }

1
1. x : ℤ
2. (|x| * 0) ≤ (|x| * |x|)
⊢ 0 ≤ (x * x)

---

Latex:

---

Latex:
\mforall{}x:\mBbbZ{}.  (0  \mleq{}  (x  *  x))


By

---

Latex:
((Auto  THEN  InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}|x|\mkleeneclose{};\mkleeneopen{}|x|\mkleeneclose{}]\mcdot{})  THEN  Auto')

---

Home Index