proposition: Lemma dominate_cut u v w: size u <= size v -> dominate u (v ++ w) -> dominate u v.
proof: Proof. Proof using. rewrite !dominate_recE. elim: u v => [// | u0 u IHu] [|v0 v] //=. by rewrite ltnS => {}/IHu Hrec /andP[-> /Hrec ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted