proposition: Lemma fin_disj_fam_prop10a A (c := fin_disj_fam_card A): fin_disj_fam A -> supp_left_unbounded c -> supp_right_unbounded c -> zint_k1 (fin_disj_fam_enum_range A).
proof: Proof. move => ha hb hc. set_extens t; [ by move/Zo_S | move => tz]. set I := (fin_disj_fam_enum_range A). have [u uI]: nonempty I. move: (hb _ ZS0) =>[j /proj31 jz /(fin_disj_fam_prop7_aux ha jz) w]; ex_tac. case:(zleT_ee tz (Zo_S uI)) => ll. exact:(fin_disj_fam_prop8l ha hb uI ll). exact:(fin_disj_fam_prop8r ha hc uI ll). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)