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