proposition: Lemma fin_disj_fam_prop5 A e1 e2 j (I := fin_disj_fam_enum_range A): fin_disj_fam A -> inc e1 I -> inc e2 I -> zbetween_eq j e1 e2 -> inc j I.
proof: Proof. move => ha /Zo_hi [x1 x1u eq1] /Zo_hi [x2 x2u eq2] [le1 le2]. move: (fin_disj_fam_prop3 ha x1u) (fin_disj_fam_prop3 ha x2u). move: (fin_disj_fam_prop2 ha). set c:= (fin_disj_fam_card A); rewrite eq1 eq2 => cf. move: (fin_disj_fam_prop1 ha x1u). set r1 := (fin_disj_fam_rank A x1); move =>[pa pb]. move: (fin_disj_fam_prop1 ha x2u). set r2 := (fin_disj_fam_rank A x2); move =>[pa2 pb2]. move: (zpartial_sum_rec cf pb2) => eq0. rewrite (zpartial_sum_rec cf pb) eq0. set s1 := zpartial_sum c r1; set s2 := zpartial_sum c r2. move => [lea leb] [lec led]. move: (zleT lea le1) (zle_ltT le2 led); rewrite -eq0 => lj1 lj2. move:(zpartial_sum_mon_spec cf pb pb2 (conj lj1 lj2)). move =>[p [pra prb] prc]. move: (fin_disj_fam_prop4 ha (proj31 prb) prc) =>[x xa ->]. apply: (fin_disj_fam_enum_range_p1 ha xa). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)