proposition: Lemma row_setK n A (i : 'I_n) (a : A) d : d `[i := a] ``_ i = a.
proof: Proof. by rewrite /row_set mxE eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2