theorem eqmcomb (a b n: nat): $ mod(n): a = b <-> mod(n): b = a $;
mod(n): a = b -> mod(n): b = a
mod(n): b = a -> mod(n): a = b
mod(n): a = b <-> mod(n): b = a