for m, n being non zero Nat holds pfexp (n lcm m) = max ((pfexp n),(pfexp m))