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