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