proposition: Lemma csum_increasing1 f j: sub j (domain f) -> (csum (restr f j)) <=c (csum f).
proof: Proof. move=> sjd. apply: sub_smaller => t. rewrite /disjointU /disjointU_fam - setU_bf - setU_bf restr_d. move /setUf_P => [y yd]; rewrite LgV // => tp. apply /setUf_P; move: (sjd _ yd) => yf; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)