---

Step * of Lemma absval-divides

∀a,b:ℤ.  (|a| | b ⇐⇒ a | b)
BY
{ ((UnivCD THENA Auto) THEN (RWO "absval_unfold" 0 THENA Auto) THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    (|a|  |  b  \mLeftarrow{}{}\mRightarrow{}  a  |  b)


By

---

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

---

Home Index