theorem mdmcan1 (a b c: nat): $ a != 0 -> a * b // (a * c) = b // c $;
a != 0 -> a * b // (a * c) = b // c /\ a * b % (a * c) = a * (b % c)
a != 0 -> a * b // (a * c) = b // c