proposition: Lemma fin_disj_fam_prop10c A (c := fin_disj_fam_card A): fin_disj_fam A -> ~ supp_left_unbounded c -> supp_right_unbounded c -> zint_k3 (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: (hc _ ZS0) =>[j /proj32 jz /(fin_disj_fam_prop7_aux ha jz) w]; ex_tac. move: (fin_disj_fam_prop9l1 ha hb nei) =>[d di dp]. exists d; first exact(Zo_S di). move => t; split; [by apply: dp | move => lrd]. exact:(fin_disj_fam_prop8r ha hc di lrd). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)