∀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