proposition: Lemma dominate_take v u n : dominate u (take n v) -> dominate u v.
proof: Proof. rewrite !dominate_recE -{2}(cat_take_drop n v). elim/last_ind: {v} (drop n v) (take n v) => [| v vn IHv]/= w. by rewrite cats0. move=> {}/IHv. by rewrite -cats1 catA cats1 -!dominate_recE; exact: dominate_rcons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted