proposition: Lemma index_enum_cast_ord n m (e: n = m) : index_enum [finType of 'I_m] = [seq (cast_ord e i) | i <- index_enum [finType of 'I_n]].
proof: Proof. subst m. rewrite -{1}(map_id (index_enum [finType of 'I_n])). apply eq_map=>[[x xlt]]. rewrite /cast_ord; congr Ordinal; apply bool_irrelevance. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)