proposition: Lemma enum_rankK_in x0 A Ax0 : {in A, cancel (@enum_rank_in T 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 seq choice) mathcomp(path div)