∀[n,m,k:ℕ].  (lcm(n;lcm(m;k)) = lcm(lcm(n;m);k) ∈ ℤ)
{ Auto }
1. n : ℕ
2. m : ℕ
3. k : ℕ
⊢ lcm(n;lcm(m;k)) = lcm(lcm(n;m);k) ∈ ℤ