proposition: Lemma csum_of_small_b2 x f: csum_of_small1 x f -> csum f <=c (x *c (domain f)).
proof: Proof. by move=> [p1 p2]; apply: (csum_of_small_b1); split => // i /p2 []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)