proposition: Lemma not_receivable_prop_uniform : ~~ receivable_prop (`U HC) W y = (\sum_(t0 in C) W ``(y | t0) == 0).
proof: Proof. apply/idP/idP => [|/eqP]. - rewrite negb_exists => /forallP H. rewrite (eq_bigr (fun=> 0)) ?big_const ?iter_addR ?mulR0 // => i iC. move: (H i). rewrite negb_and !negbK => /orP[|/eqP //]. by rewrite -(negbK (_ == _)) fdist_uniform_supp_neq0 iC. - have : forall i : 'rV_n, i \in C -> (0 <= W ``(y | i))%mcR by []. move/psumr_eq0P => H /H {}H. rewrite /receivable_prop; apply/negP. case/existsP => z /andP[]. by rewrite fdist_uniform_supp_neq0 => /H ->; rewrite eqxx. 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