---

Step * of Lemma gcd_sym_nat

∀a,b:ℕ.  (gcd(a;b) ~ gcd(b;a))
BY
{ (Auto THEN (Assert gcd(a;b) ~ gcd(b;a) BY Auto) THEN RWO "assoced_nelim" (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}.    (gcd(a;b)  \msim{}  gcd(b;a))


By

---

Latex:
(Auto  THEN  (Assert  gcd(a;b)  \msim{}  gcd(b;a)  BY  Auto)  THEN  RWO  "assoced\_nelim"  (-1)  THEN  Auto)

---

Home Index