`itv_partition` can be defined over the more general type than `realType`

[IshiguroYoshihiro]

https://github.com/math-comp/analysis/blob/1f462809ae6cfdddeea2c6a64ae36d1398063944/theories/realfun.v#L1927

itv_partition is now defined over R : realType as seq R with two conditions. However, the definition of itv_partition uses only the equality and an order structure of R. So itv_partition can be defined over more general type.