---

Step * of Lemma absval_square

∀[x:ℤ]. (|x * x| = (x * x) ∈ ℤ)
BY
{ (InstLemma `square_non_neg` [] THEN ParallelLast THEN (RWO "absval_unfold" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `square\_non\_neg`  []
  THEN  ParallelLast
  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index