fact: Record OrderedAlgebra (M : Monad) : Type := mkOrderedAlgebra { oalg_alg :> MonadAlgebra M ; oalg_rel : relation (malg_carrier oalg_alg) ; oalg_order : PreOrder oalg_rel ; oalg_mono : forall A, Proper (pointwise_relation A oalg_rel ==> pointwise_relation (M A) oalg_rel) (fun k m => oalg_alg (map k m))}.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)