theorem :: COMPLEX1:73

for a, b being Real holds min (a,b) = ((a + b) - |.(a - b).|) / 2