add more option-included lemmas

The Some_included_refl basically complement Some_included_mono as the two ways to "construct" a Some a ≼ Some b.

Some_valid_included is a version of cmra_valid_included, because applying cmra_valid_included when you have Some a ≼ Some b around is rather frustrating (mostly because Coq lacks good tactics for that kind of forward reasoning).