proposition: Lemma GE_I_incP E x: inc x (GE_I E) <-> [/\ pairp x, P x = Q x & inc (P x) E].
proof: Proof. split. by move =>/Zo_P [/setX_P [ha hb hc] hd]; split. by move => [pa pb pc]; apply:Zo_i => //; apply: setX_i => //; rewrite - pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)