proposition: Lemma enum_rankK_in x0 A Ax0 : {in A, cancel (@enum_rank_in x0 A Ax0) enum_val}.
proof: Proof. by move=> x; apply: nth_enum_rank_in. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)