proposition: Lemma compare_sum_prod5 x : fgraph x -> cardinal_pos_fam x -> \csup (range x) <=c cprod x.
proof: Proof. move => fx xi. set A := Zo (domain x) (fun a => \2c <=c (Vg x a)). have pa: (forall i, inc i ((domain x) -s A) -> (Vg x i) = \1c). move=> i /setC_P [idx ] /Zo_P h. move: (xi _ idx) => [xx yy]; ex_middle x1; case: h; split => //. apply: (cge2 (proj32 xx) (nesym yy) x1). have Ax: sub A (domain x) by apply: Zo_S. set g := (Lg A (Vg x)). have fgg: fgraph g by rewrite /g ; fprops. have dg: domain g = A by rewrite /g; aw. have gs: (forall i : Set, inc i (domain g) -> \2c <=c Vg g i). by rewrite /g dg => i iA; rewrite LgV//; move: iA => /Zo_P [_]. have cs: cardinal_set (range x). move => t /(range_gP fx) [z zy ->]; exact: (proj32_1(xi _ zy)). move: (compare_sum_prod1 fgg gs); rewrite (cprod_one_unit Ax pa) - /g. case: (emptyset_dichot A) => Ae. move: pa; rewrite Ae cprod_trivial0 setC_0 => h _. apply: (card_ub_sup CS1) => i/(range_gP fx) [t /h -> ->]; fprops. apply: cleT. have pb: (forall a, inc a (domain g) -> cardinalp (Vg g a)). by move => a /gs /proj32. move: Ae => [a Aa]; move: (Aa) => /Zo_P [ay]. have ->: Vg x a = Vg g a by rewrite /g LgV. rewrite -dg in Aa; move: (csum_increasing6 (pb _ Aa) Aa). move => le1 le2; move: (cleT le2 le1) => le3. apply: (card_ub_sup (proj32 le3)) => i /(range_gP fx) [j jdx ->]. have s1:= (cleT cle_12 le3). case: (inc_or_not j A) => jA. rewrite -dg in jA; move: (csum_increasing6 (pb _ jA) jA). rewrite {1}/g LgV//; ue. have jc: inc j ((domain x) -s A) by apply /setC_P. by rewrite (pa _ jc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)