proposition: Lemma fdist_rVS n (x : 'rV[A]_n.+1) (P : fdist R A) : P `^ n.+1 x = P (x ``_ ord0) * P `^ n (rbehead x).
proof: Proof. rewrite 2!fdist_rVE big_ord_recl; congr (_ * _). by apply eq_bigr => i _; rewrite /rbehead mxE. 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