for m, n being Nat holds n + m = n +^ m