proposition: Lemma rlmm_comp_assoc : forall i : I, left_assoc_rlmm_comp i = right_assoc_rlmm_comp i.
proof: Proof. move=> i. cbv. rewrite -!ord_cat_law3. f_equal. rewrite ord_functor_law2. reflexivity. Qed.
imports: Coq(ssreflect) Mon(SPropBase) Relational(OrderEnrichedCategory)