proposition: Lemma freeN_combination n (s : n.-tuple E) : ~~ free s -> exists k : 'I_n -> R, (\sum_i k i *: s`_i = 0) /\ exists i, k i != 0.
proof: Proof. exact: freeN_combination. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)