proposition: Theorem finite_sum_lt f g: finite_int_fam f -> finite_int_fam g -> domain f = domain g -> (forall i, inc i (domain f) -> (Vg f i) <=c (Vg g i)) -> (exists2 i, inc i (domain f) & (Vg f i) <c (Vg g i)) -> (csum f) <c (csum g).
proof: Proof. move=> [f2 f3] [g2 g3] df ale [i ifg lti]. have idg: inc i (domain g) by rewrite -df. have dtc:=(sym_eq (setC1_K ifg)). have incd: ~ (inc i ((domain f) -s1 i)). by move=> /setC1_P [_ ]; aw. have sd: sub ((domain f) -s1 i) (domain f) by apply: sub_setC. have sdg: sub ((domain g) -s1 i) (domain g) by apply: sub_setC. rewrite (induction_sum1 dtc incd). rewrite df in dtc incd; rewrite (induction_sum1 dtc incd). apply: csum_Mlelt lti. by apply: finite_sum_finite_aux. apply: csum_increasing; fprops; aww; first by ue. move=> x xd;rewrite !LgV// - ?df;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)