fact: Definition marginal1_cast (i : 'I_n.+1) (v : 'rV[A]_#|[set i]|) : A := (castmx (erefl, cards1 i) v) ``_ ord0.
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