Add derived ≼ connective on the BI level.

For !930 (closed) it was useful to have the ≼ connective on the BI level.

I originally defined it for uPreds, but since it has seen usage for non-uPred bis, I have generalized it.
Current location is at bi/lib/cmra.v.

This MR is turning out to be a bit larger than I expected, after I started moving all useful lemmas from !930 (closed) on ≼ here. It currently contains the following changes:

• Defining the ≼ connective, proofmode support for it, and some useful lemmas
• Moving some lemmas on excl and csum that were stated for uPreds, but provable for general bis with ≡.
• Add two additional hints for ≼ on the Prop level, which makes eauto more useful.