proposition: Lemma fdist_take_all (A : finType) (n : nat) (P : R.-fdist 'rV[A]_n.+2) : fdist_take P (lift ord0 ord_max) = P.
proof: Proof. rewrite /fdist_take (_ : row_take (lift ord0 ord_max) = ssrfun.id) ?fdistmap_id //. rewrite boolp.funeqE => v; apply/rowP => i. by rewrite /row_take mxE castmxE /= cast_ord_id; congr (v _ _); exact: val_inj. 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