proposition: Lemma commute_sym {A B} (ma : M A) (mb : M B) : commute ma mb -> commute mb ma.
proof: Proof. move=> /(commute_elim (fun p => ret (swap p))) //=. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)