proposition: Lemma Sprod_Ir A E x: inc x (Sprod A (GE_I E)) <-> [/\ pairp x, pairp (P x), pairp (Q x), Q (P x) = Q (Q x) & inc (Q (P x)) E /\ inc (J (P (P x)) (P (Q x))) A].
proof: Proof. split. move/Sprod_P => [a1 [a2 [b1 [b2 [r1 r2 ->]]]]]. move/GE_I_incP: r2; aw; move => [_ r3 r4];split; fprops. move=> [h1 h2 h3 h4 [h5 h6]]; rewrite -h1 - h2 - h3; apply/Sprod_P. exists (P (P x)), (Q (P x)), (P (Q x)), (Q (Q x)); split => //. apply/GE_I_incP; split; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)