proposition: Lemma fin_disj_fam_prop8l A s t (I := (fin_disj_fam_enum_range A)): fin_disj_fam A -> supp_left_unbounded (fin_disj_fam_card A) -> inc t I -> s <=z t -> inc s I.
proof: Proof. move => ha hb ti lst. move:(fin_disj_fam_prop2 ha) => cf. pose x := zpartial_sum (fin_disj_fam_card A). move: (supp_left_unbounded_p1 cf (proj31 lst) hb) =>[i iz ip]. have lt1: BZpred (x i) <z (x i). by apply:(BZsum_Mms (proj31 ip)); apply: (BZopp_positive1 ZpsS1). move: (supp_left_unbounded_p1 cf (proj31_1 lt1) hb) =>[j jz jp]. move: (zle_ltT jp lt1) => lt2. move: (zpartial_sum_mon_bis cf jz iz lt2) => /proj1 lij. move: (fin_disj_fam_prop7 ha lij lt2) => qr. apply: (fin_disj_fam_prop5 ha qr ti). by split => //; exact: (zleT (proj1 lt2) ip). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)