for a, b, n being Nat holds a |^ n,(a - b) |^ n are_congruent_mod b