proposition: Lemma index_enum_cast_ord n m (e : n = m) : index_enum (ordinal_finType m) = [seq cast_ord e i | i <- index_enum (ordinal_finType n)].
proof: Proof. subst m; rewrite -{1}(map_id (index_enum (ordinal_finType n))). apply eq_map=> [[x xlt]]. by rewrite /cast_ord; congr Ordinal; exact: bool_irrelevance. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist