proposition: Lemma csum_increasing6 f j: cardinalp (Vg f j) -> inc j (domain f) -> (Vg f j) <=c (csum f).
proof: Proof. move=> cf jd. move: (csum_increasing1 (set1_sub jd)). by rewrite csum_trivial4 (card_card cf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)