proposition: Lemma head_ofE : head_of_fdist_rV P = fdistmap (@marginal1_cast ord0) (@Subvec.d R A n.+1 P [set ord0]).
proof: Proof. apply fdist_ext => a. rewrite fdistmapE /= /head_of_fdist_rV fdist_fstE /= /head_of_fdist_rV. under eq_bigr do rewrite fdistmapE /=. rewrite /Subvec.d. under [in RHS] eq_bigr do rewrite fdistmapE /=. Abort. End subvec_prop. Section fdist_prod_nth. Local Open Scope ring_scope. Variable R : realType. Local Open Scope vec_ext_scope. Variables (A B : finType) (n : nat) (P : R.-fdist ('rV[A]_n * B)) (i : 'I_n). Definition fdist_prod_nth : R.-fdist (A * B) := fdistmap (fun x : 'rV[A]_n * B => (x.1 ord0 i, x.2)) P. Lemma fdist_prod_nthE ab : fdist_prod_nth ab = \sum_(x : 'rV[A]_n * B | (x.1 ``_ i == ab.1) && (x.2 == ab.2)) P x. Proof. by rewrite fdistmapE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext