proposition: Lemma nth_enum_rank x0 : cancel enum_rank (nth x0 (enum T)).
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)