proposition: Lemma nth_enum_rank_in x00 x0 A Ax0 : {in A, cancel (@enum_rank_in x0 A Ax0) (nth x00 (enum A))}.
proof: Proof. move=> x Ax; rewrite /= insubdK ?nth_index ?mem_enum //. by rewrite cardE [_ \in _]index_mem mem_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)