proposition: Lemma freeon_notin t d n0 V : freeon V d t -> n0 \notin V -> d ``_ n0 = t ``_ n0.
proof: Proof. move/forallP/(_ n0)/implyP => H1 H2; by rewrite (eqP (H1 H2)). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2