---

Step * 1 of Lemma exp_assoced


1. n : ℕ+@i
2. x : ℤ@i
3. y : ℤ@i
4. x^n ~ y^n@i
⊢ x ~ y
BY
{ (RepeatFor 2 (ParallelLast) THEN BLemma `exp-divides-exp2` THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}@i
2.  x  :  \mBbbZ{}@i
3.  y  :  \mBbbZ{}@i
4.  x\^{}n  \msim{}  y\^{}n@i
\mvdash{}  x  \msim{}  y


By

---

Latex:
(RepeatFor  2  (ParallelLast)  THEN  BLemma  `exp-divides-exp2`  THEN  Auto)

---

Home Index