proposition: Lemma fin_disj_fam_prop10b A (c := fin_disj_fam_card A): fin_disj_fam A -> supp_left_unbounded c -> ~supp_right_unbounded c -> zint_k4 (fin_disj_fam_enum_range A).
proof: Proof. move => ha hb hc. set I := (fin_disj_fam_enum_range A). have nei: nonempty I. move: (hb _ ZS0) =>[j /proj31 jz /(fin_disj_fam_prop7_aux ha jz) w]; ex_tac. move: (fin_disj_fam_prop9r1 ha hc nei) =>[d di dp]. exists d; first exact(Zo_S di). move => t; split; [by apply: dp | move => lrd]. exact:(fin_disj_fam_prop8l ha hb di lrd). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)