Revise the theory of the monotone CMRA

In reference to #414 (closed): I just used monotone, and I have some relevant suggestions with a concrete implementation.

I've also simplifies some proofs using set_solver.

• Type inference sometimes prefers principal_injN over principal_inj_instance (as shown by the included test), which hinders some proofs — that's easily fixed, but principal_injN might warrant more revisions (see below).
• Because of CmraDiscrete (mraR R), maybe the theory about dist (A := mra R) should be removed.
  • This MR removes almost all of this theory.
• I used the mra_over_ofe theory over a leibnizO OFE, but that theory holds for an arbitrary relation S over A, as long as R "respects S" in the right way — tying it to ofes seems potentially artificial.
  • Here I make such instances opt-in via #[export]; by default, I only export the theory relevant to S := (=), which is only principal_inj.