proposition: Lemma dominate_tl a u b v : dominate (a :: u) (b :: v) -> dominate u v.
proof: Proof. Proof using. by rewrite !dominate_recE => /= /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted