theorem :: NAT_3:53

for m, n being non zero Nat holds pfexp (n gcd m) = min ((pfexp n),(pfexp m))