proposition: Lemma Sprod_case4 s E x (f := (s \cg (Sprod (GE_I E) s)) \cg (GE_J E)): sub s ((E \times E) \times E) -> (inc x f <-> exists a b c d t, [/\ x = J (J (J a b) c) d, inc (J (J a t) d) s & inc (J (J b c) t) s]).
proof: Proof. move => h; split. move => /Zo_P [/setX_P [ha hb hc]] [y hd he]. move /GE_J_P: hd => [u [v [w [uE vE wE]]]] => eqa. move:(pr1_def eqa) (pr2_def eqa) => eqb eqc. move/(Sprod_case3 _ h): he => [a [b [c [d [t [eqd ra rb]]]]]]. move:(pr1_def eqd) (pr2_def eqd) => eqe eqf. rewrite eqe in eqc. have av:=(pr1_def eqc). have bv:=(pr1_def (pr2_def eqc)). have cv:=(pr2_def (pr2_def eqc)). by exists a,b,c,d,t; split => //; rewrite av bv cv - eqb - eqf ha. move => [a [b [c [d [t [xv ha hb]]]]]]. move/setXp_P:(h _ hb) => [/setXp_P [bE cE] tE]. move/setXp_P:(h _ ha) => [/setXp_P [aE _] dE]. have ra: inc (J (J a b) c) (domain (GE_J E)). by rewrite GE_J_domain; apply: setXp_i => //; apply:setXp_i. have rb: inc d (range (s \cg Sprod (GE_I E) s)). apply/funI_P; exists (J (J a (J b c)) d); aw;trivial. by apply/(Sprod_case3 _ h); exists a,b,c,d,t. have rc: inc x (domain (GE_J E) \times range (s \cg Sprod (GE_I E) s)). by rewrite xv;apply: setXp_i. apply:(Zo_i rc);exists (J a (J b c)). by rewrite xv; aw; apply /GE_J_P; exists a,b,c. apply/(Sprod_case3 _ h). by exists a,b,c,(Q x),t; split => //; rewrite xv;aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)