proposition: Lemma count_gt_dominate r1 r0 n : dominate r1 r0 -> (count (>%O n) r1) <= (count (>%O n) r0).
proof: Proof. Proof using. move=> /dominateP[Hsz Hdom]. rewrite -[r0](mkseq_nth inh) -[r1](mkseq_nth inh) /mkseq !count_map. rewrite -(subnKC Hsz). rewrite iotaD count_cat. set s0 := (X in X + _). apply (@leq_trans s0); last exact: leq_addr. rewrite {}/s0 -!size_filter. set f1 := (X in filter X ); set f0 := (X in _ <= size (filter X _)). rewrite (eq_in_filter (a1 := f1) (a2 := predI f1 (gtn (size r1)))); first last. by move=> i; rewrite mem_iota /= add0n => ->; rewrite andbT. rewrite (eq_in_filter (a1 := f0) (a2 := predI f0 (gtn (size r1)))); first last. by move=> i; rewrite mem_iota /= add0n => ->; rewrite andbT. rewrite !size_filter; apply sub_count => i /=. rewrite {}/f1 {}/f0 => /= /andP[Hn Hi]. rewrite Hi andbT. exact: lt_trans (Hdom i Hi) Hn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted