proposition: Lemma fdist_rV_of_prodK n : cancel (@fdist_prod_of_rV R A n) (@fdist_rV_of_prod R A n).
proof: Proof. move=> P; apply/fdist_ext => v. by rewrite fdist_rV_of_prodE fdist_prod_of_rVE row_mx_rbehead. 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