proposition: Lemma post_probE (x : 'rV[A]_n) (y : P.-receivable W) : P `^^ W (x | y) = \Pr_(P `X (W ``^ n))[ [set x] | [set receivable_rV y]].
proof: Proof. rewrite fdist_post_probE /jcPr setX1 2!Pr_set1 fdist_prodE /=. rewrite -RdivE; last first. rewrite -receivable_propE. by case: y. congr (_ / _). by rewrite fdist_sndE /=; apply eq_bigr => x' _; rewrite fdist_prodE /= -RmultE mulRC. 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