proposition: Lemma lift_range {aT rT: Type} [f: aT -> rT] (s: seq rT) : all (fun u => u \in range f) s -> exists s', map f s' = s.
proof: Proof. elim: s=>[| a s IHs]. by exists nil. move=> /andP [/set_mem [a' _ ae] /IHs [s' se]]; subst a s. by exists (a' :: s'). Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)