proposition: Lemma ex9G_P x: inc x ex9_G <-> [/\ pairp x, inc (Q x) I & inc (P x) (Vg E (Q x))].
proof: Proof. split; first by case/disjointU_P; rewrite dE. by move => [ha hb hc]; apply /disjointU_P; rewrite dE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)