fact: Definition prob_of (R : realType) := fun phT : phant (Num.NumDomain.sort R) => @prob R.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)