proposition: Lemma dominate_rcons v u l : dominate u v -> dominate u (rcons v l).
proof: Proof. Proof using. rewrite !dominate_recE. by elim: u v => [// | u0 u IHu] [|v0 v] //= /andP[-> /IHu->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted