proposition: Lemma freeon_refl V (t : 'rV[A]_n) : freeon V t t.
proof: Proof. by apply/forallP => n0; rewrite eqxx implybT. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2