proposition: Lemma rmon_id_law3 {A} : μ ∙ μ ∼ μ ∙ fmap M (rmon_id_mult A).
proof: Proof. cbv. rewrite -!relmon_law3 !cat_law3 (relmon_law2 M0) cat_law2 cat_law1. reflexivity. Qed.
imports: Coq(ssreflect ssrfun) Coq.Classes(RelationClasses Morphisms) Relational(Category)