proposition: Lemma distrib_union2_inter f g: nonempty (domain f) -> nonempty (domain g) -> (intersectionb f) \cup (intersectionb g) = intersectionf((domain f) \times (domain g)) (fun z => ((Vg f (P z)) \cup (Vg g (Q z)))).
proof: Proof. move => nef neg. have nep:nonempty ((domain f) \times (domain g)). by move: nef neg=> [x xd][y yd]; exists (J x y); fprops. set_extens x => xu. apply: (setIf_i nep)=> j /setX_P [pj p1 p2]; case /setU2_P: xu=>p. by move: (setIb_hi p p1)=>a; fprops. by move: (setIb_hi p p2)=>a; fprops. case: (inc_or_not x (intersectionb f))=> p; [fprops | apply: setU2_2]. move: nef neg; move/domain_set0P => nef1 /domain_set0P neg1. have [z1 z1d nexv]: (exists2 z1, inc z1 (domain f) & ~ (inc x (Vg f z1))). ex_middle bad;case: p. apply: (setIb_i nef1) => i id; ex_middle xx; case: bad; ex_tac. apply: (setIb_i neg1) => i id; move /(setIf_P _ nep): xu => h. by move: (h _ (setXp_i z1d id)); aw; case/setU2_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)