proposition: Lemma disjointU_hi f x: inc x (disjointU f) -> [/\ inc (Q x) (domain f), inc (P x) (Vg f (Q x)) & pairp x].
proof: Proof. move/setUb_P => [t]; rewrite disjointU_d => td. by rewrite LgV //; move /indexed_P => [pa pb ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)