proposition: Lemma row_dominate (u v : seq T) : is_row (u ++ v) -> dominate u v -> u = [::].
proof: Proof. Proof using. case: u => [// | u0 u] /=. case: v => [// | v0 v] /= /order_path_min -/(_ le_trans)/allP Hall. rewrite dominate_recE /= => /andP[Habs]; exfalso. have /Hall : v0 \in u ++ v0 :: v by rewrite mem_cat in_cons eq_refl /= orbT. by rewrite leNgt Habs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted