proposition: Lemma freeNE n (X : n.-tuple vT) : ~~ free X = [exists i : 'I_n, X`_i \in <<drop i.+1 X>>%VS].
proof: Proof. by rewrite freeE -negb_exists negbK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)