Monadic bind for `option` is non-expansive.

Just one instnace.

theories/algebra/ofe.v

@@ -959,6 +959,9 @@ Arguments optionC : clear implicits.
 Instance option_fmap_ne {A B : ofeT} n:
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
 Proof. intros f f' Hf ?? []; constructor; auto. Qed.
+Instance option_mbind_ne {A B : ofeT} n :
+  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@option_bind A B).
+Proof. destruct 2; simpl; try constructor; auto. Qed.
 Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
   CofeMor (fmap f : optionC A → optionC B).
 Instance optionC_map_ne A B : NonExpansive (@optionC_map A B).