proposition: Lemma compare_sum_prod1: csum g <=c cprod g.
proof: Proof. case: (cleT_el (CS_nat NS3) (CS_cardinal (domain g))); last first. move/(cltSleP NS2); case/cle_eqVlt. move/set_of_card_twoP => ddg; move: (ddg)=> [a [b [aneb vdg]]]. have dd: doubleton_fam g (Vg g a) (Vg g b). by split => //; rewrite -{1} (Lg_recovers fgg) Lg_range vdg funI_set2. rewrite - (cprod2_pr dd) -(csum2_pr dd). apply:(compare_sum_prod0); apply: hg; rewrite vdg; fprops. rewrite - succ_one;move/(cltSleP NS1); case/cle_eqVlt. move/set_of_card_oneP =>[x dgs]. rewrite(cprod_trivial1 dgs)(csum_trivial1 dgs); apply:cleR; fprops. move/clt1 => /card_nonempty dge. rewrite (csum_trivial dge)(cprod_trivial dge); exact:cle_01. move/ cardinal_ge3 =>[i [k1 [k2 [idg k1dg k2dg [ik1 ik2 k12]]]]]. rewrite /cprod /csum. set Pr := (productb g); set (Sr := (disjointU g)). suff [h2 [hp6 hp8]]: exists h2, ( (forall j x, inc j (domain g) -> inc x (Vg g j) -> inc (h2 j x) Pr) /\ (forall j k x y, inc j (domain g) ->inc k (domain g) -> h2 j x = h2 k y -> (x = y /\ j = k))). set hh:= Lf (fun z => h2 (Q z) (P z)) (disjointU g) (productb g). rewrite /Sr /Pr. have ->: (disjointU g) = source hh by rewrite /hh; aw. have ->: (productb g) = target hh by rewrite /hh; aw. apply: inj_source_smaller; apply: lf_injective. by move=> z zf; move: (disjointU_hi zf) => [p1 p2 p3]; apply: hp6. move=> u v ud vd; move: (disjointU_hi ud) => [p1 p2 p3]. move: (disjointU_hi vd) => [p4 p5 p6] eq. by move: (hp8 _ _ _ _ p1 p4 eq) => [sp sq]; apply: pair_exten. have gp j: inc j (domain g) -> inc \0c (Vg g j) /\ inc \1c (Vg g j). move =>jdf; move: (proj33 (hg jdf)); rewrite - (proj2 (proj2 constants_v)). move => h; split; apply:h; fprops. pose hh j x:= Lg (domain g) (fun z => Yo (z = j) x \0c). have hp1: forall j x, inc j (domain g) -> inc x (Vg g j) -> inc (hh j x) Pr. move => j x jdf xv; apply /setXb_P;rewrite /hh; aw; split;fprops. move => z zdf. rewrite LgV//; Ytac zj; [ ue | exact:(proj1 (gp _ zdf))]. have hp2: forall j x y, inc j (domain g) -> (hh j x = hh j y) -> x = y. by move=> j x y jdf sh;move:(f_equal (Vg^~j) sh);rewrite/hh !LgV//;Ytac0;Ytac0. have hp3: forall j k x y, inc j (domain g) -> inc k (domain g)-> j <> k -> (hh j x = hh k y) -> (x = \0c /\ y = \0c). move=> j l x y jdf ldf jl sh;split. by move: (f_equal (Vg^~ j) sh); rewrite /hh !LgV//; Ytac0; Ytac0. by move: (f_equal (Vg^~ l) sh); rewrite /hh !LgV//; Ytac0; Ytac0. pose h1 j := Lg (domain g) (fun z => Yo (z = j) \0c \1c). have hp4: forall j, inc j (domain g) -> inc (h1 j) Pr. move => j jdf; apply /setXb_P;rewrite /h1 Lgd;split;fprops. by move=> z zdf; rewrite LgV//; move:(gp _ zdf) => [za zb]; Ytac zj. have hp5: forall j j', inc j (domain g) -> (h1 j = h1 j') -> j = j'. move=> j j' jdf sh;ex_middle jj'; move: (f_equal (Vg ^~j) sh). by rewrite /h1 ! LgV//;Ytac0; Ytac0 => /esym e01; case: card1_nz. pose h2 j x := Yo (x = \0c) (h1 j) (hh j x). exists h2; split. move=> j x jdf xV; rewrite /h2; Ytac e1; [by apply: hp4 | by apply: hp1]. have hp7: forall j k x, inc j (domain g) ->inc k (domain g) -> hh j x <> h1 k. move=> j k x jdf kdf; rewrite /hh /h1. suff [z [zdf z1 z2]]: (exists z, [/\ inc z (domain g), z <> j & z <> k]). move=> eq; move: (f_equal (Vg ^~z) eq). by rewrite !LgV//; Ytac0; Ytac0; fprops. case: (equal_or_not j i) => ji. case: (equal_or_not k k1) => kk1. - exists k2; rewrite ji kk1;split; fprops. - exists k1; rewrite ji; split;fprops. case: (equal_or_not k i) => kk1; last by exists i; split; fprops. case: (equal_or_not k1 j) => jk2. exists k2; rewrite kk1 - jk2; split; fprops. exists k1; rewrite kk1; split; fprops. move=> j k x y jdf kdf; rewrite /h2; Ytac e1. Ytac e2. by move=> sh1; move: (hp5 _ _ jdf sh1) => aux; rewrite e1 e2 aux. by move => aux; case: (hp7 _ _ y kdf jdf). Ytac e2 => sh1; first by case: (hp7 _ _ x jdf kdf). case: (equal_or_not j k) => e3. split => //;rewrite e3 in sh1; apply: (hp2 _ _ _ kdf sh1). by move: (hp3 _ _ _ _ jdf kdf e3 sh1) => [aux1 aux2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)