proposition: Lemma fin_disj_fam_prop4 A i e: fin_disj_fam A -> intp i -> zbetween e (zpartial_sum (fin_disj_fam_card A) i) (zpartial_sum (fin_disj_fam_card A) (BZsucc i)) -> exists2 x, inc x (unionb A) & e = fin_disj_fam_enum A x.
proof: Proof. move => h1 iz. move: (fin_disj_fam_prop2 h1); set c:= (fin_disj_fam_card A) => cf. move: (zpartial_sum_int cf iz); rewrite (zpartial_sum_rec cf iz). move => az [le1 lt2]. move: (proj32 le1) => ez. move/(zle_diffP az ez): le1; move: (BZ_valN (ZS_diff ez az)). move: (BZsum_diff1 az ez). set d := e -z _ => dv dN dp. move: (BZp_hi_pr dp) => eq1. have qa: natp (Vg c i) by move:cf =>[ra rv rc]; apply: rc; ue. move: lt2; rewrite - {1} dv BZsumC. move/(BZsum_lt2l (BZp_sBZ dp) (ZNz qa) az); rewrite - eq1. move/(zlt_cN dN qa) => /(NltP qa) lt3. have fsai: finite_set (Vg A i) by move: h1 =>[qsa qb qc qd]; apply: qd; ue. move: (simple_enump (Vg A i)). have -> : (cardinal (Vg A i)) = Vg c i by rewrite /c /fin_disj_fam_card; bw. move => [[_ sjf] sf tf]. rewrite -tf in lt3; move: (proj2 sjf _ lt3); rewrite sf; move => [x x1 etc]. move: (fin_disj_fam_prop1_bis h1 iz x1) => [xu idx]; exists x => //. by rewrite /fin_disj_fam_enum idx - etc eq1 BZsum_diff. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)