theorem :: INT_7:11
for n, m, k being non zero Nat st k = n gcd m holds
support (ppf k) = (support (ppf n)) /\ (support (ppf m))