proposition: Lemma fin_disj_fam_prop9l1 A (I := (fin_disj_fam_enum_range A)): fin_disj_fam A -> ~ supp_left_unbounded (fin_disj_fam_card A) -> nonempty I -> exists2 i, inc i I & forall a, inc a I -> i <=z a.
proof: Proof. move => ha hc [u uI]. pose M d := (forall a, inc a I -> d <=z a). case:(all_exists_dichot2 M I) => // H. move:(fin_disj_fam_prop9l ha hc) => [b bz bp]. have aux: forall i, b <=z i -> M (BZsucc i). apply:BZ_induction_pos. move => a aI. apply/(zlt_succ2P bz (Zo_S aI)); split; first by apply: bp. by move => ba; case: (H a aI); rewrite - ba. move => n bn Ms a ai; move: (Ms a ai) => q. apply/(zlt_succ2P (ZS_succ (proj32 bn)) (proj32 q)); split => // ee. by case:(H a ai); rewrite - ee. case:(H u uI); move:(bp _ uI); case (equal_or_not b u) => ee; first by ue. move => ll; move: (proj32 ll) => uz. by move/ (zlt_pred1P bz (proj32 ll)): (conj ll ee) => /aux; rewrite BZsucc_pred. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)