---

Step * of Lemma absval-diff-symmetry

∀[x,y:ℤ].  (|x - y| ~ |y - x|)
BY
{ (Auto THEN RWO "absval_unfold" 0 THEN Repeat (AutoSplit) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbZ{}].    (|x  -  y|  \msim{}  |y  -  x|)


By

---

Latex:
(Auto  THEN  RWO  "absval\_unfold"  0  THEN  Repeat  (AutoSplit)  THEN  Auto')

---

Home Index