proposition: Lemma ord_cat_le_comp : f ⪷ f' -> g ⪷ g' -> g ∙ f ⪷ g' ∙ f'.
proof: Proof. move=> Hf Hg. eapply Comp_proper. assumption. assumption. Qed.
imports: Coq(Relation_Definitions) Relational(OrderEnrichedCategory) Mon(SPropBase) mathcomp(all_ssreflect boolp) Crypt(Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions)