fact: Definition F_choice_prod_obj : Obj (prod_cat ord_choiceType ord_choiceType) -> Obj ord_choiceType.
imports: Mon(SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(all_ssreflect)