proposition: Lemma fin_disj_fam_prop8r A s t (I := (fin_disj_fam_enum_range A)): fin_disj_fam A -> supp_right_unbounded (fin_disj_fam_card A) -> inc t I -> t <=z s -> 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_right_unbounded_p1 cf (proj32 lst) hb) =>[i iz ip]. have lt1: x i <z (BZsucc (x i)) by apply:(BZsum_Mps (proj32 ip) ZpsS1). move: (supp_right_unbounded_p1 cf (proj32_1 lt1) hb) =>[j jz jp]. move: (zlt_leT lt1 jp) => lt2. move: (zpartial_sum_mon_bis cf iz jz lt2) => /proj1 lij. move: (fin_disj_fam_prop7 ha lij lt2) => qr. by apply: (fin_disj_fam_prop5 ha ti qr). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)