for r being Real ex n being Nat st - n <= r