---

Step * of Lemma sign-squared

∀[x:ℤ]. ((sign(x) * sign(x)) = 1 ∈ ℤ)
BY
{ (Auto THEN Unfolds ``sign absval`` 0 THEN SplitOnConclITE THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  ((sign(x)  *  sign(x))  =  1)


By

---

Latex:
(Auto  THEN  Unfolds  ``sign  absval``  0  THEN  SplitOnConclITE  THEN  Auto)\mcdot{}

---

Home Index