proposition: Lemma enum_val_ord n i : enum_val i = cast_ord (card_ord n) i.
proof: Proof. by apply: canLR (@enum_rankK _) _; apply: val_inj; rewrite enum_rank_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)