The Coq mailing list

[brandon_m_moore AT yahoo.com]

> These modules are already given in the standard library, look in
> theories/Structures/OrderedTypeEx.v for Nat_as_OT for example.

Thanks. That answers the problem of getting a Nat_as_OT suitable for FMap.

It doesn't seem to provide a general conversion functor, which might not be
that useful overall, but would at least be applicable for cases such as Q
(maybe for an FSet).