proposition: Lemma compg_P r r' x: inc x (r' \cg r) <-> (pairp x /\ (exists2 y, inc (J (P x) y) r & inc (J y (Q x)) r')).
proof: Proof. split;first by move/Zo_P => [pa pb];split => //; apply: (setX_pair pa). move => [pa pb]; apply: Zo_i => //. move: pb => [z pc pd];apply/setX_P;split => //; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)