proposition: Theorem finite_product_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)) -> card_nz_fam g -> (cprod f) <c (cprod g).
proof: Proof. move=> [f2 f3] [g2 g3] df ale [i ifg lti] alne. have idg: inc i (domain g) by rewrite -df. have afN: natp (Vg f i) by apply: f2. have agN: natp (Vg g i) by apply: g2. 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. have incd: ~ (inc i ((domain f) -s1 i)). by move=> /setC1_P [_ ]; aw => aux; case: aux. move: (setC1_K ifg) => /esym dtc. rewrite (induction_prod1 dtc incd). rewrite df in dtc incd; rewrite (induction_prod1 dtc incd). apply: cprod_Mlelt =>//. + by apply: finite_product_finite_aux. + apply: cprod_increasing;aww; first by ue. move=> x xd; rewrite !LgV// - ?df;fprops. + apply/cprod_nzP; fprops; hnf;aw => j jdg. move: (jdg) => /setC1_P [jd _]; rewrite LgV//;apply: (alne _ jd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)