for k being Nat
for n being prime Nat
for a, b being positive Nat holds (n * a) * b divides ((((a,b) In_Power n) | n) /^ 1) . k