proposition: Lemma commute_ret {A B} (a : A) (mb : M B) : commute (ret a) mb.
proof: Proof. rewrite /commute /bind monad_law1 ; f_equal. extensionality a2; rewrite monad_law1 //. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)