proposition: Lemma count_lt_le_mem x s : (count (< x) s < count (<= x) s)%N = (x \in s).
proof: Proof. have := count_predUI (pred1 x) (< x) s. have -> : count (predI (pred1 x) (< x)) s = 0%N. rewrite (@eq_count _ _ pred0) ?count_pred0 // => y /=. by rewrite lt_def; case: eqP => //= ->; rewrite eqxx. have /eq_count-> : [predU1 x & < x] =1 (<= x) by move=> y /=; rewrite le_eqVlt. by rewrite addn0 => ->; rewrite -add1n leq_add2r -has_count has_pred1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)