GCD


THEOREM    \(\forall x \in \mathbb{S} : \gcd(x, y) \mid x\)
gcd_dvd1: gcd ?a ?b dvd ?a

Proof unavailable

THEOREM    \(\forall x \in \mathbb{S} : \gcd(x, y) \mid y\)
gcd_dvd2: gcd ?a ?b dvd ?b

Proof unavailable