proposition: Lemma basisEdim X U : basis_of U X = (U <= <<X>>)%VS && (size X <= \dim U).
proof: Proof. apply/andP/idP=> [[defU /eqnP <-]| ]; first by rewrite -eqEdim eq_sym. case/andP=> sUX leXU; have leXX := dim_span X. rewrite /free eq_sym eqEdim sUX eqn_leq !(leq_trans leXX) //. by rewrite (leq_trans leXU) ?dimvS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)