proposition: Lemma compare_sum_prod f g: fgraph f -> fgraph g -> domain f = domain g -> (forall i, inc i (domain f) -> Vg f i <c Vg g i) -> csum f <c cprod g.
proof: Proof. move=> fgf fgg sd ale1. set K:= Zo (domain f) (fun i => \2c <=c (Vg g i)). have kdf: sub K (domain f) by apply: Zo_S. have kdg: sub K (domain g) by ue. have aux: forall i, inc i ((domain f) -s K) -> (Vg f i = \0c /\ Vg g i = \1c). move=> i => /setC_P [idf] /Zo_P aux. have le1:=(ale1 _ idf). case: (cleT_el CS2 (proj32_1 le1)); first by move=> h; case: aux;split => //. rewrite - succ_one ; move /(cltSleP NS1) => h1. have p1:=(clt1 (clt_leT le1 h1)). split => //; apply: (cleA h1). by move: le1; rewrite p1; move/cge1P. have pf:(forall i, inc i ((domain f) -s K) -> Vg f i = \0c). by move=> i ic; move: (aux _ ic) => []. have pg:(forall i, inc i ((domain g) -s K) -> Vg g i = \1c). by rewrite - sd;move=> i ic; move: (aux _ ic) => []. rewrite (csum_zero_unit kdf pf) (cprod_one_unit kdg pg). apply: compare_sum_prod3; aww. by hnf; aw; move=> i iK; rewrite LgV//; move: iK => /Zo_P //; case. by move=> i iK; rewrite !LgV//; apply: ale1; apply: kdf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)