proposition: Lemma eq_enum_rank_in (x0 y0 : T) A (Ax0 : x0 \in A) (Ay0 : y0 \in A) : {in A, enum_rank_in Ax0 =1 enum_rank_in Ay0}.
proof: Proof. by move=> x xA; apply: enum_val_inj; rewrite !enum_rankK_in. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)