move CMRA to its own file, in anticipation ofn a dependency to SPred that would otherwise have induced a cycle
add metric-pair-map functions; remove duplicate map functions; define an order on nonexp functions with an ordered codomain
BI are an extension of "bounded"
Conflicts: coq-ho/lib/ModuRes/Finmap.v
Conflicts: coq-ho/lib/ModuRes/BI.v
