proposition: Lemma fin_disj_fam_prop9r A (I := (fin_disj_fam_enum_range A)): fin_disj_fam A -> ~ supp_right_unbounded (fin_disj_fam_card A) -> exists2 i, intp i & forall a, inc a I -> a <z i.
proof: Proof. move => ha hb. move:(fin_disj_fam_prop2 ha) => cf. move: (supp_right_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. case: (proj2(zle_ltT qa qb)). by rewrite (jp _ lij) (jp _ (zleT lij (proj1(zlt_succ jz)))). by move/(zlt_succ2P jz iz): lij => /(zpartial_sum_mon cf); apply: zlt_leT. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)