proposition: Lemma le_enum_rank_in x0 A (Ax0 : x0 \in A) : {in A &, {mono enum_rank_in Ax0 : x y / x <= y}}.
proof: Proof. apply: can_mono_in (@in2W _ _ predT predT _ (@le_enum_val A)) => //. exact/onW_can_in/enum_rankK_in. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)