---

Step * 1 1 of Lemma divides_anti_sym


1. a : ℤ
2. b : ℤ
3. |a| | |b|
4. |b| | |a|
⊢ a = ± b
BY
{ (Rewrite (RevLemmaC `absval_eq`) 0 THENA Auto) }

1
1. a : ℤ
2. b : ℤ
3. |a| | |b|
4. |b| | |a|
⊢ |a| = |b| ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
(Rewrite  (RevLemmaC  `absval\_eq`)  0  THENA  Auto)

---

Home Index