proposition: Lemma pr_eq_neq0 (X : {RV P -> A}) (a : A) : `Pr[ X = a ] != 0 <-> exists i, i \in X @^-1 a /\ 0 < P i.
proof: Proof. split; rewrite pr_eqE /Pr => PXa0. have H : forall i : U, 0 <= P i by move=> ?; apply/RleP/FDist.ge0. have := proj1 (@sumR_neq0 U P (enum (finset (X @^-1 a))) H). by rewrite !big_enum /= => /(_ PXa0) [i]; rewrite mem_enum inE => ?; exists i. case: PXa0 => i ?; rewrite -big_enum; apply/sumR_neq0; by [move=> ?; exact/RleP/FDist.ge0 | exists i; rewrite mem_enum inE]. 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