proposition: Lemma rbelast_row_mx (x : 'rV_n) a : rbelast (castmx (erefl 1%N, addn1 n) (row_mx x (\row_(j < 1) a))) = x.
proof: Proof. apply/rowP => i; rewrite !(mxE,castmxE) /=; case: splitP => [j /= ij|k /=]. by congr (x _ _); apply/val_inj. rewrite (ord1 k) addn0 => ni; move: (ltn_ord i); by rewrite ni ltnn. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2