theorem eqmax1 (a b: nat): $ b <= a -> max a b = a $;
max a b = max b a
b <= a -> max b a = a
b <= a -> max a b = a