proposition: Lemma receivable_propE (y : P.-receivable W) : receivable_prop P W y = (\sum_(x in 'rV[A]_n) P x * W ``(y | x) != 0).
proof: Proof. apply/idP/idP => [|H]. - case/existsP => /= x /andP[Px0]. apply: contra => /eqP /psumr_eq0P => /= H. apply/eqP; rewrite -(@eqR_mul2l (P x)); last exact/eqP. by rewrite mulR0 H // => /= x' _; rewrite RmultE mulr_ge0//. - have /= : \sum_(x in setT) P x * W ``(y | x) != 0. apply: contra H => /eqP H; apply/eqP. rewrite -[RHS]H; apply/eq_bigl => /= x; by rewrite !inE. apply: contraNT. rewrite /receivable_prop negb_exists => /forallP /= {}H. apply/eqP/big1 => x _. by move: (H x); rewrite negb_and 2!negbK => /orP[|] /eqP ->; rewrite ?(mul0R,mulR0). 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