proposition: Lemma dominateP u v : reflect (size u <= size v /\ forall i, i < size u -> (nth inh u i > nth inh v i)%O) (dominate u v).
proof: Proof. Proof using. rewrite /dominate /mkseq ; apply/(iffP idP). - move=> /andP[Hsz /allP Hall]; split; first exact Hsz. by move=> i Hi; apply: Hall; rewrite mem_iota add0n. - by move=> [] -> /= H; apply/allP => i; rewrite mem_iota add0n; apply: H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted