fact: Definition rFreeProb_squ_fromProd := product_rmon rFreePr rFreePr.
imports: mathcomp(all_ssreflect boolp) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd choice_type) Crypt(SubDistr)