proposition: Lemma isum_q6 I x: inc x (disjointU (restr f I)) <-> [/\ inc (Q x) I, inc (P x) (Vg f (Q x)) & pairp x].
proof: Proof. apply: (iff_trans (@disjointU_P (Lg I (Vg f)) x)). rewrite Lgd; split => - [qa qb qc]; split => //; move: qb;rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)