proposition: Lemma cprod_increasing1 f j: card_nz_fam f -> sub j (domain f) -> (cprod (restr f j)) <=c (cprod f).
proof: Proof. move=> alne sjd; rewrite cprod_pr cprod_pr /cprodb; aw. set f' := Lg (domain f) (fun z => cardinal (Vg f z)). pose (g:= Lg (domain f) (fun z => Yo (inc z j) (cardinal (Vg f z)) \1c)). have fgg: fgraph g by rewrite /g; fprops. have dgdf : domain g = domain f by rewrite /g; aw. have ->: (Lg j (fun a : Set => cardinal (Vg (restr f j) a))) = Lg j (Vg g). by apply: Lg_exten => a aj;rewrite /g !LgV// ; [ Ytac0 | apply: sjd]. have <-: (cprod g = cprod (Lg j (Vg g))). apply: cprod_one_unit=>//; rewrite dgdf //. by move=> i /setC_P [idf nij]; rewrite /g LgV // Y_false. rewrite/g/f';apply: cprod_increasing; aw; trivial. move => x xdg; rewrite !LgV //; Ytac h; fprops. apply: cge1; fprops; exact:(card_nonempty0 (alne x xdg)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)