proposition: Lemma filter_gt_dominate r1 r0 n : is_row r0 -> is_row r1 -> dominate r1 r0 -> dominate (filter (>%O n) r1) (filter (>%O n) r0).
proof: Proof. Proof using. move=> Hrow0 Hrow1 Hdom. have Hsize := count_gt_dominate n Hdom. move: Hdom => /dominateP[Hsz Hdom]. apply/dominateP; rewrite !size_filter. split; first exact Hsize. move=> i Hi. rewrite (filter_gt_row _ Hrow0) (filter_gt_row _ Hrow1) !nth_take. - by apply Hdom; apply (leq_trans Hi); apply: count_size. - exact: Hi. - exact: (leq_trans Hi). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted