for r, s being Real holds max+ (r + s) <= (max+ r) + (max+ s)