proposition: Lemma dominate_head u v : u != [::] -> dominate u v -> (head inh v < head inh u)%O.
proof: Proof. Proof using. by rewrite !dominate_recE; case: u v => [// | u0 u] [|v0 v] //= _ /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted