proposition: Lemma freeon0 (t d : 'rV_n) : (freeon set0 t d) = (t == d).
proof: Proof. apply/forallP/eqP => /= [H|-> x]; last by rewrite eqxx implybT. apply/rowP => i; move: (H i); by rewrite !inE implyTb => /eqP. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2