theorem eqmtr (a b c n: nat): $ mod(n): a = b -> mod(n): b = c -> mod(n): a = c $;
a % n = b % n -> b % n = c % n -> a % n = c % n
mod(n): a = b -> mod(n): b = c -> mod(n): a = c