---

Step * of Lemma lcm-gcd-absorption

∀[n,m:ℕ].  (lcm(n;gcd(n;m)) = n ∈ ℤ)
BY
{ (Auto THEN Symmetry THEN BLemma `lcm-unique-nat` THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Symmetry  THEN  BLemma  `lcm-unique-nat`  THEN  Auto)

---

Home Index