proposition: Lemma fin_disj_fam_prop7_aux A k: fin_disj_fam A -> intp k -> Vg (fin_disj_fam_card A) k <> \0c -> inc (zpartial_sum (fin_disj_fam_card A) k) (fin_disj_fam_enum_range A).
proof: Proof. move => ha kz cnz. move:(simple_enump (Vg A k)); set f := (simple_enum _). move => [bf sf tf]. have ztf: inc \0c (target f). move: cnz; rewrite /fin_disj_fam_card; bw => // cnz. by move: (card_ne0_pos (CS_cardinal (Vg A k)) cnz) => /oclt /olt_i; ue. move: (inverse_V bf ztf) (inverse_Vis bf ztf); rewrite sf. set y := Vf (inverse_fun f) \0c => vy ys. move:(fin_disj_fam_prop1_bis ha kz ys) =>[yu ry]. set (x := zpartial_sum (fin_disj_fam_card A)). move:(zpartial_sum_int (fin_disj_fam_prop2 ha) kz) => hh. have ->: x k = (fin_disj_fam_enum A y). by rewrite /fin_disj_fam_enum ry vy (BZsum_0r). by apply: (fin_disj_fam_enum_range_p1 ha yu). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)