proposition: Theorem csum_Cn X f: target f = domain X -> bijection f -> csum X = csum (X \cf (graph f)).
proof: Proof. move=> tf [[ff injf] sjf]. have sf:source f = domain (graph f) by rewrite domain_fg. pose X' := Lg (domain X) (Vg X). pose g:= Lg (source f) (fun i => (Vg (X' \cf (graph f)) i) *s1 (Vf f i)). have ->: X \cf (graph f) = (Lg (source f) (fun z => Vg X (Vf f z))). by rewrite /composef -(proj33 ff); apply: Lg_exten => i idf; rewrite /X';aw. rewrite -(csum_gr X) /csumb /csum /disjointU/ disjointU_fam Lgd. set h := Lg _ _. have fgh: fgraph h by rewrite/h;fprops. have imfh: Imf f = domain h by rewrite (surjective_pr0 sjf) /h; aw. rewrite (setUb_rewrite1 ff fgh imfh). have aux x : inc x (source f ) -> inc (Vg (graph f) x) (domain X) by rewrite - tf; apply: Vf_target. have <-: (g = h \cf (graph f)). have sf1: source f = domain (h \cf graph f)by rewrite composef_domain. rewrite /g;apply: fgraph_exten; aww => x xsf; move: (aux _ xsf) => aa. have xdf: inc x (domain (graph f)) by ue. by rewrite !LgV. apply: Eqc_disjointU. - rewrite /g; saw => i isf; move: (aux _ isf) => aa. rewrite !LgV //; aw; trivial;ue. - rewrite /g; apply: mutually_disjoint_prop; aw => i j y isf jsf. rewrite !LgV // - ? sf //; try apply: aux => //. move /setX_P => [_ _ /set1_P e1] /setX_P [_ _ /set1_P e2]. rewrite e1 in e2; apply: (injf _ _ isf jsf e2); ue. apply:disjointU_disjoint. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)