proposition: Lemma fin_disj_fam_prop10e A (c := fin_disj_fam_card A): fin_disj_fam A -> (exists2 i, intp i & nonempty (Vg A i)) -> ~ supp_left_unbounded c -> ~ supp_right_unbounded c -> zint_k5 (fin_disj_fam_enum_range A).
proof: Proof. move => ha [i0 i9z nn] hb hc. have ru: inc (rep (Vg A i0)) (unionb A). by apply/setUb_P; exists i0; [ rewrite (proj42 ha) | apply: rep_i]. move:(fin_disj_fam_enum_range_p1 ha ru). set k := fin_disj_fam_enum _ _ => kI. have neI: nonempty (fin_disj_fam_enum_range A) by exists k. move: (fin_disj_fam_prop9l1 ha hb neI) =>[l li lp]. move: (fin_disj_fam_prop9r1 ha hc neI) =>[r ri rp]. move: (zleT (lp _ kI) (rp _ kI)) => llr. exists l, r; split => // z; split. move => zI; split; [exact:(lp _ zI) | exact:(rp _ zI)]. move => q; exact:(fin_disj_fam_prop5 ha li ri q). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)