for h, s being non zero Nat st ( for q being Prime st q in support (prime_factorization s) holds
not q,h are_coprime ) holds
support (prime_factorization s) c= support (prime_factorization h)