proposition: Lemma sorted_geq_count_leq2E (s : seq nat) : sorted geq s -> (count (leq 2) s <= 1) = (nth 0 s 1 <= 1).
proof: Proof. case: s => [|s0 [|s1 s]]//=; first by rewrite addn0; case: ltnP. move=> /andP[le10 Hpath]; case: (ltnP 1 s1) => [|les1 {le10}]. by move/leq_trans/(_ le10) ->; rewrite !add1n. suff -> : count (leq 2) s = 0 by rewrite !addn0; case: ltnP. elim: s s1 Hpath les1 => // s2 s IHs s1. move=> /= /andP[les2 Hpath /(leq_trans les2) {les2}les]. by rewrite (IHs _ Hpath les) addn0 ltnNge les. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype