proposition: Lemma csum_of_small_b1 x f: csum_of_small0 x f -> csum f <=c (x *c (domain f)).
proof: Proof. move=> [p1 p2];rewrite - csum_of_same. by apply:csum_increasing; aw => //; fprops => a adf; rewrite LgV//; apply: p2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)