1. x : ℤ
2. y : ℤ
3. gcd(x;y) ~ x
⊢ x | y
{ D (-1) }
3. gcd(x;y) | x
4. x | gcd(x;y)