proposition: Lemma dominate_recE : dominate =2 dominate_rec.
proof: Proof. Proof using. rewrite /dominate; elim=> [// | u0 u IHu] [// | v0 v] /=. rewrite -IHu ltnS [RHS]andbA [LHS]andbA [_&& (v0 < u0)%O]andbC; congr (_ && _). by rewrite -add1n iotaDl all_map; apply eq_all => i. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted