for m, n being Nat
for t being Integer holds t |^ n,t |^ m are_congruent_mod t - 1