proposition: Lemma freeon_all (t d : 'rV_n) n0 : (t ``_ n0 == d ``_ n0) = freeon (setT :\ n0) d t.
proof: Proof. apply/idP/idP => H. apply/forallP => i. rewrite !inE andbT negbK; apply/implyP => /eqP ->; by rewrite eq_sym. by rewrite (@freeon_notin t _ _ (setT :\ n0)) // !inE eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2