proposition: Lemma fdist_takeE i v : fdist_take i v = \sum_(w in 'rV[A]_(n - i)) P (castmx (erefl, subnKC (ltnS' (ltn_ord i))) (row_mx v w)).
proof: Proof. rewrite fdistmapE /=. rewrite (@reindex_onto _ _ _ [finType of 'rV[A]_n] [finType of 'rV[A]_(n - i)] (fun w => castmx (erefl 1%nat, subnKC (ltnS' (ltn_ord i))) (row_mx v w)) (@row_drop A n i)) /=; last first. move=> w wv; apply/rowP => j. rewrite castmxE /= cast_ord_id /row_drop mxE; case: splitP => [j0 /= jj0|k /= jik]. - rewrite -(eqP wv) mxE castmxE /= cast_ord_id; congr (w _ _); exact: val_inj. - rewrite mxE /= castmxE /= cast_ord_id; congr (w _ _); exact: val_inj. apply eq_bigl => w; rewrite inE; apply/andP; split; apply/eqP/rowP => j. - by rewrite !mxE !castmxE /= !cast_ord_id esymK cast_ordK row_mxEl. - by rewrite !mxE !castmxE /= cast_ord_id esymK cast_ordK cast_ord_id row_mxEr. 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