---

Step * 1 1 1 of Lemma divides_anti_sym


1. a : ℤ
2. b : ℤ
3. |a| | |b|
4. |b| | |a|
⊢ |a| = |b| ∈ ℤ
BY
{ (BLemma `divides_anti_sym_n` ⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  |a|  |  |b|
4.  |b|  |  |a|
\mvdash{}  |a|  =  |b|


By

---

Latex:
(BLemma  `divides\_anti\_sym\_n`  \mcdot{}  THEN  Auto)

---

Home Index