proposition: Lemma fin_disj_fam_prop6 A: fin_disj_fam A -> {inc (unionb A) &, injective (fin_disj_fam_enum A)}.
proof: Proof. move => Ha a b au bu sv. move: (fin_disj_fam_prop3 Ha au)(fin_disj_fam_prop3 Ha bu). move: (fin_disj_fam_prop1 Ha au)(fin_disj_fam_prop1 Ha bu). move: (fin_disj_fam_prop2 Ha). set u := (fin_disj_fam_rank A a). set v := (fin_disj_fam_rank A b). set c := (fin_disj_fam_card A). rewrite - sv; move => cf [au1 uz] [bu1 vz] [la lb][lc ld]. have luv: u <=z v. move:(zle_ltT la ld). set x := zpartial_sum c u. set y := zpartial_sum c (BZsucc v) => lxx. move: (zpartial_sum_mon_spec cf uz vz (conj (zleR (proj31_1 lxx)) lxx)). move => [p [pa pb] _]; apply: (zleT pa pb). have lvu: v <=z u. move:(zle_ltT lc lb). set x := zpartial_sum c v. set y := zpartial_sum c (BZsucc u) => lxx. move: (zpartial_sum_mon_spec cf vz uz (conj (zleR (proj31_1 lxx)) lxx)). move => [p [pa pb] _]; apply: (zleT pa pb). move: (zleA luv lvu) => euv. move: sv. have fsA: finite_set (Vg A u). apply/card_finite_setP; move: cf =>[qa qb qc]. have ->: cardinal (Vg A u) = Vg c u by rewrite /c /fin_disj_fam_card; bw. apply: qc; ue. have sa := proj1 (simple_enump2 fsA au1). rewrite - euv in bu1. have sb := proj1 (simple_enump2 fsA bu1). rewrite /fin_disj_fam_enum -/c -/u -/v - euv. move /(BZsum_eq2l (zpartial_sum_int cf uz) (ZNz sa) (ZNz sb)). move/BZ_of_nat_inj. move: (simple_enump (Vg A u)) =>[[[_ fi] _] sf _]. by apply: fi; rewrite sf. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)