theorem Th58: :: NAT_3:58

for a, b being non zero Nat st a,b are_coprime holds
ppf (a * b) = (ppf a) + (ppf b)