proposition: Lemma fin_disj_fam_prop9l A (I := (fin_disj_fam_enum_range A)): fin_disj_fam A -> ~ supp_left_unbounded (fin_disj_fam_card A) -> exists2 i, intp i & forall a, inc a I -> i <=z a.
proof: Proof. move => ha hb. move:(fin_disj_fam_prop2 ha) => cf. move: (supp_left_unbounded_p2 cf hb) =>[i iz ]. set x := zpartial_sum (fin_disj_fam_card A) => jp. have xiz: intp (x i) by apply: zpartial_sum_int. exists (x i) => // e /Zo_P [ez [a au ea]]. move:(fin_disj_fam_prop1 ha au); set j := (fin_disj_fam_rank A a). move => [aAi jz]. move:(fin_disj_fam_prop3 ha au); rewrite ea -/x -/j; move => [qa qb]. case: (zleT_el iz jz) => lij. exact: (zleT (zpartial_sum_mon cf lij) qa). case: (proj2(zle_ltT qa qb)); rewrite (jp _ (proj1 lij)). by move/(zlt_succ2P jz iz): lij => /jp ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)