proposition: Lemma GE_J_P E x: inc x (GE_J E) <-> exists a b c, [/\ inc a E, inc b E, inc c E & x = (J (J (J a b) c) (J a (J b c)))].
proof: Proof. split. move /Zo_P => [/setX_P]. move => [h1 /setX_P[h2 /setX_P[h3 h4 h5] h6] /setX_P[h7 h8 /setX_P[h9 _ _]]]. move => [ra rb rc]. exists (P (P (P x))), (Q (P (P x))), (Q (P x)); split => //. by rewrite h3 h2 ra rb rc h9 h7 h1. move=> [a [b [c [ sa sb sc ->]]] ]; apply /Zo_P; split; aw => //. by apply:setXp_i; apply: setXp_i => //; apply: setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)