proposition: Lemma supp_F2_to_GF2 n m (e : 'rV['F_2]_n) : supp (F2_to_GF2 m e) = supp e.
proof: Proof. apply/setP => i; rewrite !inE !mxE; apply/idP/idP; apply: contra. move/eqP => ->; by rewrite rmorph0. by rewrite GF2_of_F2_eq0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2 mathcomp(finfield)