Strenghten `cmra_valid_elim` and derive `cmra_valid_discrete`.

Old:

Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.

New:

Lemma cmra_valid_elim {A : cmra} (a : A) : ✓ a ⊢ ⌜ ✓{0} a ⌝.

The old version is rather weak because it is impossible to derive positive information from it. It seems it is also not used.

I noticed that Perennial has the new version already: https://github.com/mit-pdos/perennial/blob/master/src/algebra/own_discrete.v#L7

Other advantage: We can derive cmra_discrete now, it no longer needs to be primitive.