proposition: Lemma dimv_compl U : \dim U^C = (\dim {:vT} - \dim U)%N.
proof: Proof. by rewrite dimvf /dimv mxrank_gen mxrank_compl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)