proposition: Lemma compare_sum_prod2: (forall i, inc i (domain f) -> Vg f i <=c Vg g i) -> csum f <=c cprod g.
proof: Proof. move=> ale1. exact: (cleT (csum_increasing sd ale1) (compare_sum_prod1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)