proposition: Lemma not_trivialP : not_trivial <-> C != 0%VS.
proof: Proof. split; rewrite /not_trivial. - case => x /andP[xC]. apply: contra => /eqP C0; move: xC; by rewrite C0 memv0. - rewrite -vpick0 => C0. exists (vpick C); by rewrite C0 andbT memv_pick. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2