proposition: Lemma enum_rank_ord n i : enum_rank i = cast_ord (esym (card_ord n)) i.
proof: Proof. apply: val_inj; rewrite /enum_rank enum_rank_in.unlock. by rewrite insubdK ?index_enum_ord // card_ord [_ \in _]ltn_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)