proposition: Lemma trmx_cV_0 {k} (x : 'cV['F_2]_k) : (x ^T == 0) = (x == 0).
proof: Proof. case Hlhs : (_ ^T == _). symmetry. move/eqP in Hlhs. by rewrite -(trmxK x) Hlhs trmx0 eqxx. symmetry; apply/eqP. move=> abs; subst x. by rewrite trmx0 eqxx in Hlhs. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2