proposition: Lemma fin_disj_fam_prop7 A i j (x := zpartial_sum (fin_disj_fam_card A)): fin_disj_fam A -> i <=z j -> x i <z x j -> inc (x i) (fin_disj_fam_enum_range A).
proof: Proof. move => ha lij lvij. move: (fin_disj_fam_prop2 ha); set c := (fin_disj_fam_card A) => cf. move: (lij) =>[iz jz _]. have: exists k, [/\ i <=z k, x i = x k & x k <z x (BZsucc k)]. ex_middle bad. have h: forall k, i <=z k -> x i = x k. apply: BZ_induction_pos => // n lin Hr. rewrite Hr;ex_middle ne; case: bad; exists n; split => //; split => //. have le: n <=z BZsucc n by apply: (BZsum_Mp (proj32 lin) (BZps_sBZp ZpsS1)). exact: (zpartial_sum_mon cf le). by case: (proj2 lvij); apply: h. move =>[k [/proj32 kz ->]]. rewrite {2}/x (zpartial_sum_rec cf kz) -/x; move=>[le1]. case: (equal_or_not (Vg c k) \0c) => dz ww. by move: ww; rewrite dz (BZsum_0r (proj31 le1)); case. exact:(fin_disj_fam_prop7_aux ha kz dz). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)