proposition: Lemma basisEfree X U : basis_of U X = [&& free X, (<<X>> <= U)%VS & \dim U <= size X].
proof: Proof. by rewrite andbC; apply: andb_id2r => freeX; rewrite eqEdim (eqnP freeX). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)