Step * 1 1 1 of Lemma divides_anti_sym


1. : ℤ
2. : ℤ
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