proposition: Lemma fdist_rV_of_prodE a : fdist_rV_of_prod a = P (a ``_ ord0, rbehead a).
proof: Proof. rewrite /fdist_rV_of_prod fdistmapE /=. rewrite {1}(_ : a = f (a ``_ ord0, rbehead a)); last first. by rewrite /f /= row_mx_rbehead. by rewrite (big_pred1_inj inj_f). 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