proposition: Lemma commute_bind {A1 A2 B} (m1 : M A1) (f1 : A1 -> M A2) (m2:M B) : commute m1 m2 -> (forall a1, commute (f1 a1) m2) -> commute (bind m1 f1) m2.
proof: Proof. move=> Hm Hf ; rewrite /commute /bind monad_law3. repeat rewrite -/bind. under eq_bind => a1 do rewrite (Hf a1). apply_commute_elim Hm. under eq_bind => b do rewrite /bind -monad_law3. done. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)