proposition: Lemma inj_row_set (A : ringType) n n0 (d : 'rV_n) : {in A &, injective ((row_set n0)^~ d)}.
proof: Proof. move=> a b _ _ /= /rowP /(_ n0); by rewrite mxE eqxx mxE eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2