---

Step * of Lemma gcd_com

∀[n,m:ℕ].  (gcd(n;m) ~ gcd(m;n))
BY
{ (Auto THEN InstLemma `gcd_sym` [⌜n⌝;⌜m⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].    (gcd(n;m)  \msim{}  gcd(m;n))


By

---

Latex:
(Auto  THEN  InstLemma  `gcd\_sym`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index