for r, s being Real st 0 <= r & s * s < r * r holds
s < r