∀a,b,n:ℤ.  ((n * gcd(a;b)) ~ gcd(n * a;n * b))
{ Auto }
1. a : ℤ
2. b : ℤ
3. n : ℤ
⊢ (n * gcd(a;b)) ~ gcd(n * a;n * b)