let a, b, c be Real; :: thesis: ( 0 <= c implies c * (max (a,b)) = max ((c * a),(c * b)) )

assume A1: 0 <= c ; :: thesis: c * (max (a,b)) = max ((c * a),(c * b))

assume A1: 0 <= c ; :: thesis: c * (max (a,b)) = max ((c * a),(c * b))

per cases
( max (a,b) = b or max (a,b) = a )
by XXREAL_0:16;

end;