fact: Record OrderedMonadAlgebra : Type := mkOrderedMonadAlgebra { omalg_alg :> MonadAlgebra OM ; omalg_rel : relation (malg_carrier omalg_alg) ; omalg_order : PreOrder omalg_rel ; omalg_mono : forall A, Proper (pointwise_relation A omalg_rel ==> (@omon_rel OM A) ==> omalg_rel) (fun k m => omalg_alg (map k m))}.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)