proposition: Lemma fin_disj_fam_prop9r1 A (I := (fin_disj_fam_enum_range A)): fin_disj_fam A -> ~ supp_right_unbounded (fin_disj_fam_card A) -> nonempty I -> exists2 i, inc i I & forall a, inc a I -> a <=z i.
proof: Proof. move => ha hc [u uI]. pose M d := (forall a, inc a I -> a <=z d). case:(all_exists_dichot2 M I) => // H. move:(fin_disj_fam_prop9r ha hc) => [b bz bp]. move/(zlt_pred1P (Zo_S uI) bz): (bp u uI) => ll. have aux: forall i, i <=z (BZpred b) -> M i. apply:BZ_induction_neg. by move => a aI; apply /(zlt_pred1P (Zo_S aI) bz); apply: bp. move => n na mn a aI. move:(mn a aI); case: (equal_or_not a n) => ean. by case: (H _ aI); rewrite ean. by move => lan; apply/(zlt_pred1P(proj31 lan) (proj32 lan)). case:(H u uI); exact: (aux _ ll). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)