proposition: Lemma freeon1 (F : finFieldType) {n} i (d : 'rV[F]_n) : forall t, freeon [set i] d t = (t \in [set d `[ i := x ] | x in F]).
proof: Proof. move=> t. case/boolP : (_ \in _). case/imsetP => /= x _ ->; by rewrite freeon_row_set. apply: contraNF. move/forallP => /= X. apply/imsetP => /=. exists (t ``_ i) => //. apply/rowP => b. rewrite mxE. case: ifPn => [/eqP -> //| bi]. apply/esym/eqP. move: (X b) => /implyP; apply. by rewrite in_set1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2