proposition: Lemma eq_count_merge (p : pred T) s1 s1' s2 s2' : count p s1 = count p s1' -> count p s2 = count p s2' -> count p (merge leT s1 s2) = count p (merge leT s1' s2').
proof: Proof. by rewrite !count_merge !count_cat => -> ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)