proposition: Lemma freeon_row_set n0 (d : 'rV[A]_n) x : freeon [set n0] d (d `[ n0 := x ]).
proof: Proof. apply/forallP => /= i; rewrite !inE !mxE. case/boolP : (i == n0) => //; by rewrite implyTb. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2