fact: Definition compPairRMonad (M1 M2 : rMonad): ord_relativeMonad (ord_functor_id TypeCatSq) := rmon_transp_natIso (product_rmon M1 M2) idxid_iso_id.
imports: Coq(ssreflect ssrfun ssrbool) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms RelationPairs) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory Rel)