proposition: Theorem csum_increasing f g: domain f = domain g -> (forall x, inc x (domain f) -> (Vg f x) <=c (Vg g x)) -> (csum f) <=c (csum g).
proof: Proof. move=> dfdg ale; apply: sub_smaller => t. rewrite /disjointU /disjointU_fam. move /setUb_P; aw; move => [y ydf]; rewrite LgV //. move /setX_P => [pt Pt /set1_P Qt]; apply/setUb_P; aw; rewrite -dfdg. ex_tac; rewrite LgV // -{2} Qt;apply :setX_i; fprops. by move: (ale _ ydf) => [_ _];apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)