---

Step * of Lemma gcd_unique

∀a,b,y1,y2:ℤ.  (GCD(a;b;y1) ⇒ GCD(a;b;y2) ⇒ (y1 ~ y2))
BY
{ ((Unfolds ``gcd_p assoced`` 0 THEN HypBackchain) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b,y1,y2:\mBbbZ{}.    (GCD(a;b;y1)  {}\mRightarrow{}  GCD(a;b;y2)  {}\mRightarrow{}  (y1  \msim{}  y2))


By

---

Latex:
((Unfolds  ``gcd\_p  assoced``  0  THEN  HypBackchain)  THEN  Auto)

---

Home Index