Why does rationals_le use the concrete type nat?

I was surprised when unfolding rationals_le to see that it specifies that le x y if there is a fraction p/q made of nats such that y=x+p/q:

Instance rationals_le `{Rationals Q} : Le Q | 10 := λ x y,
  ∃ num, ∃ den, y = x + naturals_to_semiring nat Q num / naturals_to_semiring nat Q den.

Why not use any type that is an instance of Naturals?

I agree. It seems better to generalize this to general instances.

Navigation Menu