fact: Definition pmf : {ffun 'I_3 -> R} := finfun [fun x => 0 with ord0 |-> 1/2, ord1 |-> 1/3, ord2 |-> 1/6].
imports: Reals Lra mathcomp(all_ssreflect ssrnum) mathcomp(Rstruct) Reals_ext ssrR realType_ext fdist proba