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

[IshiguroYoshihiro]

analysis/theories/realfun.v

Line 1927 in 1f46280

Definition itv_partition a b s := [/\ path <%R a s & last a s == b].

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.