∀x,y:ℤ.  (x | y 
⇐⇒ gcd(y;x) = x ∈ ℤ)
{ Auto }
1. x : ℤ
2. y : ℤ
3. x | y
⊢ gcd(y;x) = x ∈ ℤ
1. x : ℤ
2. y : ℤ
3. gcd(y;x) = x ∈ ℤ
⊢ x | y