proposition: Lemma post_prob_uniform_kernel (x : 'rV[A]_n) : (`U HC) `^^ W (x | y) = (K * (x \in C)%:R * W ``(y | x))%R.
proof: Proof. case/boolP : (x \in C) => xC. - by rewrite post_prob_uniformT // ?inE // mulR1. - by rewrite post_prob_uniformF ?inE // mulR0 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