proposition: Lemma row_setC n A (i j : 'I_n) (a b : A) d : i != j -> d `[ j := b ] `[ i := a ] = d `[ i := a ] `[ j := b ].
proof: Proof. move=> ij; apply/rowP => k; rewrite !mxE. by case: ifP => // /eqP ->; case: ifPn => //; rewrite (negbTE ij). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2