proposition: Lemma post_prob_uniformF (x : 'rV[A]_n) : x \notin C -> (`U HC) `^^ W (x | y) = 0.
proof: Proof. move=> xC; rewrite fdist_post_probE fdist_uniform_supp_notin //. by rewrite -!RmultE !mul0R. Qed.
imports: mathcomp(all_ssreflect all_algebra zmodp matrix) Reals mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext fdist proba channel jfdist_cond