proposition: Lemma dominate_trans : transitive dominate.
proof: Proof. Proof using. move=> r2 r1 r3; rewrite !dominate_recE. elim: r1 r2 r3 => [// | a1 l1] IHl [|a2 l2] [|a3 l3] //=. by move=> /andP[/(lt_trans _) Ha21 {}/IHl Hrec] /andP[/Ha21-> /Hrec->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted