An Integer That Only Decreases?

by . .

Is it correct to say that a type system needs to implement dependent types if it is to allow the expression of an integer that can only decrease? The goal would be to define a type R Integer such that a function R Integer -> R Integer would only compile if the Integer inside the output value was equal or less to the one inside the input.