proposition: Lemma post_prob_uniformT (x : 'rV[A]_n) : x \in C -> (`U HC) `^^ W (x | y) = K * W ``(y | x).
proof: Proof. move=> Ht. have C0 : INR #|C| != 0 by rewrite INR_eq0' -lt0n. rewrite fdist_post_probE fdist_uniform_supp_in //. rewrite -RinvE; last first. by rewrite -INRE. rewrite -!RmultE mulRC. rewrite -RinvE; last first. rewrite -receivable_propE. by case: y. rewrite mulRA. congr (_ * _). rewrite /den fdist_uniform_supp_restrict. rewrite -invRM//. 3: by rewrite -INRE. rewrite /K /post_prob_uniform_cst; congr Rinv. rewrite !RmultE -INRE. rewrite big_distrl /=. apply eq_bigr => i iC. rewrite fdist_uniform_supp_in //. rewrite GRing.mulrAC INRE GRing.mulVr ?GRing.mul1r//. by rewrite GRing.unitfE -INRE. rewrite (eq_bigr (fun t => 1 / INR #|C| * W ``(y | t))); last first. move=> *; rewrite fdist_uniform_supp_in//. by rewrite GRing.div1r INRE. apply/eqP; rewrite -big_distrr /= mulR_eq0 => -[]. by rewrite -RdivE// div1R; apply/invR_neq0/eqP. by apply/eqP; rewrite -not_receivable_prop_uniform receivableP. 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