fact: Definition row_set B n (n0 : 'I_n) (x : B) (d : 'rV_n) := \row_(i < n) if i == n0 then x else d ``_ i.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2