proposition: Lemma csum_commutative1 f x: csum_of_small1 x f -> exists g, [/\ csum_of_small1 x g, domain g = cardinal (domain f), csum f = csum g & range g = range f].
proof: Proof. move=> [fgf pb]. move: (CS_cardinal (domain f)) => [ocy cyp]. set z1 := cardinal (domain f). have /card_eqP [g [bg sg tg]]: z1 =c (domain f) by rewrite /z1; aw. set h := Lg z1 (fun i => Vg f (Vf g i)). have dh: domain h = z1 by rewrite /h; aw. have fgh: fgraph h by rewrite /h; fprops. have sh: forall i, inc i (domain h) -> Vg h i <c x. rewrite /h; aw => i id; rewrite LgV//; apply: pb. rewrite - tg; apply: Vf_target; try fct_tac; ue. have ch: cardinal_fam h by move => a ay; exact: (proj31_1 (sh _ ay)). have fg: function g by fct_tac. have rh: range h = range f. rewrite /h; set_extens t. move/(range_gP fgh); rewrite dh; move => [u p1 ->]; rewrite /h LgV //. apply /(range_gP fgf); exists (Vf g u)=> //; rewrite -tg; Wtac. move /(range_gP fgf) => [u p1 ->]; apply/(range_gP fgh). rewrite - tg in p1; move: ((bij_surj bg) _ p1) => [w usg ww]. rewrite /h; rewrite dh - sg; ex_tac; rewrite LgV// ; ue. exists h => //; split => //. have ->: h = f \cf (graph g). rewrite /composef /h /Vf. have -> //: domain (graph g) = z1 by rewrite domain_fg. apply: csum_Cn => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)