proposition: Lemma nth_filter [T : Type] (P: {pred T}) x (s: seq T) n : (n < size [seq i <- s | P i])%N -> P (nth x [seq i <- s | P i] n).
proof: Proof. elim: s n=> [| a s IHs] n //=. case Pa: (P a). 2: by apply IHs. by case: n=>//=; rewrite ltnS; apply IHs. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)