proposition: Lemma Eq_powsum a b c: functions (dsum b c) a \Eq functions b a \times functions c a.
proof: Proof. rewrite candu2_rw. move:(Eq_pow_inv (EqR a) (Eq_indexed b C0)) => qb. move:(Eq_pow_inv (EqR a) (Eq_indexed c C1)) => qc. apply: EqT (EqS (Eq_mul_inv qb qc)). move:(disjointU2_pr b c C0_ne_C1). set B := b *s1 C0; set C := c *s1 C1 => dbc. apply: EqT (EqS (Eq_mul_inv (Eq_fun_set B a) (Eq_fun_set C a))). apply: (EqT (Eq_fun_set (B \cup C) a)). apply: EqS; clear qb qc. exists (Lf (fun z => (P z \cup Q z)) (gfunctions B a \times gfunctions C a)(gfunctions (B \cup C) a)). saw;apply: lf_bijective. - move => u /setX_P[pi /gfunctions_P1 [qa qb qc] /gfunctions_P1 [qd qe qf]]. apply/gfunctions_P1; split. + by apply: fgraph_setU2 => //; rewrite qb qe. + by rewrite domain_setU2 qb qe. + rewrite set2_UXl. move => t/setU2_P; case; [ move/ qc | move/ qf]; fprops. - move => u v /setX_P[pu /gfunctions_P1 [qa qb qc] /gfunctions_P1 [qd qe qf]]. move => /setX_P[pv /gfunctions_P1 [ra rb rc] /gfunctions_P1 [rd re rf]] sv. apply: (pair_exten pu pv). set_extens t => tp. have /setU2_P: inc t (P v \cup Q v) by rewrite - sv; apply: setU2_1. case => // /rf /setX_P[_ h1 _]; move:(qc _ tp) => /setX_P[_ h2 _]. empty_tac1 (P t). have /setU2_P: inc t (P u \cup Q u) by rewrite sv; apply: setU2_1. case => // / qf /setX_P[_ h1 _]; move:(rc _ tp) => /setX_P[_ h2 _]. empty_tac1 (P t). set_extens t => tp. have /setU2_P: inc t (P v \cup Q v) by rewrite - sv; apply: setU2_2. case => // /rc /setX_P[_ h1 _]; move:(qf _ tp) => /setX_P[_ h2 _]. empty_tac1 (P t). have /setU2_P: inc t (P u \cup Q u) by rewrite sv; apply: setU2_2. case => // / qc /setX_P[_ h1 _]; move:(rf _ tp) => /setX_P[_ h2 _]. empty_tac1 (P t). move => y /gfunctions_P1 [qa qb] ;rewrite set2_UXl => qc. set y1 := y \cap (B \times a); set y2 := y \cap (C \times a). have tv: y = P (J y1 y2) \cup Q (J y1 y2). aw; set_extens t; last by case/setU2_P => /setI2_P []. move => ty; case/setU2_P:(qc _ ty) => tt. by apply: setU2_1;apply: setI2_i. by apply: setU2_2;apply: setI2_i. exists (J y1 y2) => //; apply:setXp_i. apply/gfunctions_P1; split => //. + by apply:(sub_fgraph qa) => t /setI2_P; case. + set_extens t. by move=> /funI_P[z /setI2_P [_ /setX_P [_ h _]] ->]. move => tc. have /funI_P [s rb rc]: inc t (domain y) by rewrite qb; fprops. apply/funI_P; exists s => //; apply:setI2_i => //. case/setU2_P:(qc _ rb) => // /setX_P [_ h _]. empty_tac1 (P s); ue. + by move => t /setI2_P; case. apply/gfunctions_P1; split => //. + by apply:(sub_fgraph qa) => t /setI2_P; case. + set_extens t. by move=> /funI_P[z /setI2_P [_ /setX_P [_ h _]] ->]. move => tc. have /funI_P [s rb rc]: inc t (domain y) by rewrite qb; fprops. apply/funI_P; exists s => //; apply:setI2_i => //. case/setU2_P:(qc _ rb) => // /setX_P [_ h _]. empty_tac1 (P s); ue. + by move => t /setI2_P; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)