The cmra_op_discrete lemma is entirely unused so far from what I can tell. @jtassaro is using a variant of it in Perennial, but it turns out the lemma needs to be strengthened a bit to fit. This MR upstreams the strengthened version.
I preserved the original statement as cmra_op_discrete', but honestly I doubt that it is worth keeping. So @robbertkrebbers if you're fine with that I'd just remove it.