proposition: Lemma cat_basis U V X Y : directv (U + V) -> basis_of U X -> basis_of V Y -> basis_of (U + V) (X ++ Y).
proof: Proof. move=> dxUV /andP[/eqP defU freeX] /andP[/eqP defV freeY]. by rewrite /basis_of span_cat cat_free defU defV // eqxx freeX freeY. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)