theorem :: IDEA_1:12

for i, j, n being Nat holds ADD_MOD (i,j,n) = ADD_MOD (j,i,n) ;