fact: Definition acto : UU0 -> UU0 := fun A => {dist (choice_of_Type A)}.
imports: Reals mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals Rstruct) infotheo(Reals_ext realType_ext ssr_ext fsdist) infotheo(convex) HB(structures) monae_lib hierarchy monad_lib proba_lib