proposition: Lemma compare_sum_prod3: (forall i, inc i (domain f) -> Vg f i <c Vg g i) -> csum f <c cprod g.
proof: Proof. move=> alt1. have ale1: (forall i, inc i (domain f) -> (Vg f i) <=c (Vg g i)). by move => i idf; move: (alt1 _ idf) => [ok _]. split; first by apply: compare_sum_prod2. move /card_eqP=> [h [bh sh th]]. pose D i := (Vg f i) *s1 i. have Dp1: forall i, inc i (domain f) -> sub (D i) (source h). move=> i idf t td; rewrite sh; apply /setUb_P. rewrite /disjointU_fam; aw; ex_tac; rewrite LgV//. pose A i := Vfs h (D i). have Dp2: forall i, inc i (domain f) -> (cardinal (A i)) <c (Vg g i). move: (bh) => [ih _]. move=> i idf;move: (alt1 _ idf) => aux. rewrite /A (cardinal_image (Dp1 _ idf) ih) (cardinal_indexed). by rewrite (card_card (proj31_1 aux)). have fh: function h by fct_tac. have Dp3: forall i, inc i (domain f) -> sub (A i) (target h). by move=> i idf; apply: fun_image_Starget1. have Dp4: forall i F, inc i (domain f) -> sub F (target h) -> (cardinal (Vfs (pr_i g i) F)) <=c (cardinal F). rewrite th; move=> i F idf Fp; apply: surjective_cle. have idg: inc i (domain g) by ue. exists (restriction1 (pr_i g i) F). split => //; rewrite /restriction1; aw; trivial. apply: restriction1_fs; first by apply: pri_f => //. by rewrite /pr_i; aw. have Dp5: forall i, inc i (domain f) -> (cardinal (Vfs (pr_i g i) (A i))) <c (Vg g i). move=> i idf; exact:(cle_ltT (Dp4 _ _ idf (Dp3 _ idf)) (Dp2 _ idf) ). have Dp6: forall i, inc i (domain f) -> exists xi, inc xi (Vg g i) /\ (forall y, inc y (A i) -> Vf (pr_i g i) y <> xi). move=> i idf; move: (Dp5 _ idf); set T := Vfs _ _. have fp: function (pr_i g i) by apply: pri_f => //; ue. have st: sub T (Vg g i). by move: (@fun_image_Starget1 _ fp (A i)); rewrite {2} /pr_i lf_target. rewrite -{1} (card_card (proj32_1 ( (alt1 _ idf)))); move=> [_ neq]. ex_middle nex; case: neq;apply:f_equal; apply:extensionality =>//. have sAi: sub (A i) (source (pr_i g i)). by rewrite /pr_i; aw; rewrite -th; apply: Dp3. move=> x xv; apply /(Vf_image_P fp sAi). ex_middle ney; case: nex; exists x; split => //. move=> y yA;case: (equal_or_not (Vf (pr_i g i) y) x) => //. move=> wy; case: ney; ex_tac. pose k i:= choose (fun xi => inc xi (Vg g i) /\ (forall y : Set, inc y (A i) -> Vf (pr_i g i) y <> xi)). have kp: forall i, inc i (domain f) -> (inc (k i) (Vg g i) /\ (forall y, inc y (A i) -> Vf (pr_i g i) y <> (k i))). move=> i idf; apply choose_pr; apply: (Dp6 _ idf). set x := Lg (domain g) k. have xth: inc x (target h). rewrite th /x; apply /setXb_P; split;aww; move=> i idg; rewrite LgV//. by rewrite - sd in idg; move: (kp _ idg) => [p1 _]. move: bh => [ih sjh]; move: ((proj2 sjh) _ xth) => [y ysg Wy]. move: ysg; rewrite sh; move /setUb_P. rewrite/disjointU_fam;aw. move=> [i idf]; rewrite LgV// => yd. have xA: inc x (A i). by rewrite /A Wy; apply /(Vf_image_P (proj1 ih)(Dp1 _ idf)); exists y. move: (kp _ idf) => [_ p2]; move: (p2 _ xA). rewrite sd in idf; rewrite th in xth. by rewrite pri_V // /x LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)