fact: Definition left_unit := forall A, join \o ret = id :> (F A -> F A).
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra Rstruct reals) infotheo(Reals_ext) infotheo(realType_ext) monae_lib HB(structures)