for a, b being Nat
for k, l being Integer st k,l are_coprime holds
k |^ a,l |^ b are_coprime