proposition: Lemma pr_eq0 (X : {RV P -> A}) (a : A) : a \notin fin_img X -> `Pr[ X = a ] = 0.
proof: Proof. move=> aX; apply/eqP/negPn; apply: contra aX => /pr_eq_neq0 [i [iXa Pi0]]. rewrite mem_undup; apply/mapP; exists i; rewrite ?mem_enum //. by move: iXa; rewrite inE => /eqP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist