proposition: Lemma count_merge (p : pred T) s1 s2 : count p (merge s1 s2) = count p (s1 ++ s2).
proof: Proof. rewrite count_cat; elim: s1 s2 => // x s1 IH1. elim=> //= [|y s2 IH2]; first by rewrite addn0. by case: leT; rewrite /= ?IH1 ?IH2 !addnA [_ + p y]addnAC [p x + p y]addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)