proposition: Lemma Sprod_case3 s E x (f := s \cg (Sprod (GE_I E) s)): sub s ((E \times E) \times E) -> (inc x f <-> exists a b c d t, [/\ x = J (J a (J b c)) d, inc (J (J a t) d) s & inc (J (J b c) t) s]).
proof: Proof. move => sp;split. move/compg_P => [pa [y ya yb]]. move /Sprod_Il: ya;aw; move => [_ pb yc yd [ye yf]]. have ppc: pairp (Q (P x)) by move:(sp _ yf) => /setXp_P [/setX_P []]. exists (P (P x)), (P (Q (P x))), (Q (Q (P x))), (Q x), (Q y). by rewrite ppc pb pa yd yc. move => [a [b [c [d [t [ha hb hc]]]]]]. have px: pairp x by rewrite ha;fprops. have ra: inc (J (J a t) (Q x)) s by rewrite ha; aw. have aE: inc a E by move:(sp _ ra) => /setXp_P [/setX_P []]; aw. apply/compg_P; split => //; exists (J a t) => //. apply/Sprod_Il; rewrite ha;aw; split;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)