proposition: Lemma commute_elim {A B C} (f : A × B -> M C) (ma : M A) (mb : M B) : commute ma mb -> bind ma (fun a=> bind mb (fun b => f ⟨a,b⟩)) = bind mb (fun b=> bind ma (fun a=> f ⟨a,b⟩)).
proof: Proof. rewrite /commute=> /(f_equal (fun t => bind t f)). rewrite /bind !monad_law3. repeat rewrite -/bind. under eq_bind => a do (rewrite /bind !monad_law3 -/bind ; under eq_bind => b do rewrite monad_law1). under (@eq_bind B _) => a do (rewrite /bind !monad_law3 -/bind ; under eq_bind => b do rewrite monad_law1). done. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)