proposition: Lemma free_cons v X : free (v :: X) = (v \notin <<X>>)%VS && free X.
proof: Proof. rewrite (cat_free [:: v]) seq1_free directvEgeq /= span_seq1 dim_vline. case: eqP => [-> | _] /=; first by rewrite mem0v. rewrite andbC ltnNge (geq_leqif (dimv_leqif_sup _)) ?addvSr //. by rewrite subv_add subvv andbT -memvE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)