Function key_obeys_cmp_spec Copy item path

Whether the Key type obeys the cmp spec, required for BTreeMap

This is a workaround to the fact that BTreeMap “late binds” the trait bounds when needed. For instance, BTreeMap::iter does not require Key: Ord, even though it yields ordered items. Rather, it relies on the fact that BTreeMap::insert does require Key: Ord, meaning no instance of a BTreeMap will ever have keys that cannot be comparable.

See also axiom_key_obeys_cmp_spec_meaning.