proposition: Lemma free_directv X : free X = (0 \notin X) && directv (\sum_(v <- X) <[v]>).
proof: Proof. have leXi i (v := tnth (in_tuple X) i): true -> \dim <[v]> <= 1 ?= iff (v != 0). by rewrite -seq1_free -span_seq1 => _; apply/leqif_eq/dim_span. have [_ /=] := leqif_trans (dimv_sum_leqif _) (leqif_sum leXi). rewrite sum1_card card_ord !directvE /= /free andbC span_def !(big_tnth _ _ X). by congr (_ = _ && _); rewrite -has_pred1 -all_predC -big_all big_tnth big_andE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)