proposition: Lemma fdist_belast_last_of_rVE a : fdist_belast_last_of_rV a = P (castmx (erefl, addn1 n) (row_mx a.1 (\row_(i < 1) a.2))).
proof: Proof. case: a => x y; rewrite /fdist_belast_last_of_rV fdistmapE /=. rewrite (_ : (x, y) = g (castmx (erefl 1%nat, addn1 n) (row_mx x (\row__ y)))); last first. by rewrite /g rbelast_row_mx row_mx_row_ord_max. by rewrite (big_pred1_inj inj_g). 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