proposition: Lemma fin_disj_fam_prop3 A x (i := (fin_disj_fam_rank A x)): fin_disj_fam A -> inc x (unionb A) -> zbetween (fin_disj_fam_enum A x) (zpartial_sum (fin_disj_fam_card A) i) (zpartial_sum (fin_disj_fam_card A) (BZsucc i)).
proof: Proof. move => h1 h2. move: (fin_disj_fam_prop2 h1). move: (fin_disj_fam_prop1 h1 h2). rewrite /fin_disj_fam_enum -/i. set c:= (fin_disj_fam_card A). move => [pa pb] pc. have fsai: finite_set (Vg A i) by move: h1 =>[qsa qb qc qd]; apply: qd; ue. move: (simple_enump2 fsai pa); set u := Vf _ _; move => [uN le1]. have le2: u <c Vg c i by rewrite /c /fin_disj_fam_card; bw. move: (zpartial_sum_int pc pb); rewrite (zpartial_sum_rec pc pb) => h3. split; first exact:(BZsum_Mp h3 (BZ_of_natp_i uN)). have qa: natp (Vg c i) by move:pc =>[ra rv rc]; apply: rc; ue. by apply/(BZsum_lt2l (ZNz uN) (ZNz qa) h3); apply/ zlt_cN. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)