proposition: Lemma nth_count_eq x x0 s i : sorted <=%O s -> (count (< x) s <= i < count (<= x) s)%N -> nth x0 s i = x.
proof: Proof. move=> ss /andP[ige ilt]; apply/le_anti. by rewrite nth_count_le// nth_count_ge// ige (leq_trans ilt (count_size _ _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)