proposition: Lemma map_nth_ord [T : Type] (x: T) (s : seq T) : [seq nth x s (nat_of_ord i) | i <- index_enum [finType of 'I_(size s)]] = s.
proof: Proof. rewrite /index_enum; case: index_enum_key=>/=; rewrite -enumT. elim: s=>/= [| a s IHs]. by case: (enum 'I_0)=> [| s q] //; inversion s. by rewrite enum_ordSl /= -map_comp /=; congr cons. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)