proposition: Lemma row_mx_row_ord_max (x : 'rV[A]_n) a : rlast (castmx (erefl 1%nat, addn1 n) (row_mx x (\row_(k < 1) a))) = a.
proof: Proof. rewrite /rlast castmxE /= mxE /=; case: splitP => [j Hj|k _]. by move: (ltn_ord j); rewrite -Hj ltnn. by rewrite (ord1 k) mxE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2