for n, m being non zero Nat st m divides n holds
pfexp (n div m) = (pfexp n) -' (pfexp m)