proposition: Lemma supp_set0 e : (supp e == set0) = (e == 0).
proof: Proof. apply/idP/idP => [/eqP/setP HE |/eqP ]; last first. rewrite /supp => ->; by apply/eqP/setP => i; rewrite !inE /= mxE eqxx. apply/eqP/rowP => i; rewrite mxE. move: (HE i); by rewrite !inE /= => /negbT; rewrite negbK => /eqP. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2