theorem eqmin2 (a b: nat): $ b <= a -> min a b = b $;
min a b = min b a
b <= a -> min b a = b
b <= a -> min a b = b