proposition: Lemma enum_rank_index {T : finType} i : nat_of_ord (enum_rank i) = index i (enum T).
proof: Proof. rewrite /enum_rank /enum_rank_in /insubd /odflt /oapp insubT//. by rewrite cardE index_mem mem_enum. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)