proposition: Lemma enum_val_bij_in x0 A : x0 \in A -> {on A, bijective (@enum_val A)}.
proof: Proof. move=> Ax0; exists (enum_rank_in Ax0) => [i _|]; last exact: enum_rankK_in. exact: enum_valK_in. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)