proposition: Lemma sep__part_Sum2 : Partition_Sum gP incF[=] Sumx (fun (i : nat) (Hi : i < m) => Sum2 (fun (j : nat) (Hj : sep__part_fun i (Nat.lt_le_incl _ _ Hi) <= j) (Hj' : j <= pred (sep__part_fun (S i) Hi)) => F (g j (RS'_Hsep_S _ _ _ Hj')) just1[*] (P _ (RS'_Hsep_S _ _ _ Hj')[-]P _ (RS'_Hsep _ _ _ Hj')))).
proof: Proof. unfold Partition_Sum in |- *. apply eq_symmetric_unfolded. unfold Sum2 in |- *. apply eq_transitive_unfolded with (Sumx (fun (j : nat) (Hj : j < n) => part_tot_nat_fun _ _ (fun (i : nat) (H : i < n) => F (g i H) just1[*](P _ H[-]P _ (Nat.lt_le_incl _ _ H))) j)). apply str_Sumx_Sum_Sum' with (g := fun (i : nat) (Hi : i < m) (i0 : nat) => sumbool_rect (fun _ : {sep__part_fun i (Nat.lt_le_incl i m Hi) <= i0} + {i0 < sep__part_fun i (Nat.lt_le_incl i m Hi)} => IR) (fun _ : sep__part_fun i (Nat.lt_le_incl i m Hi) <= i0 => sumbool_rect (fun _ : {i0 <= pred (sep__part_fun (S i) Hi)} + {pred (sep__part_fun (S i) Hi) < i0} => IR) (fun H0 : i0 <= pred (sep__part_fun (S i) Hi) => F (g i0 (RS'_Hsep_S i i0 Hi H0)) (incF (g i0 (RS'_Hsep_S i i0 Hi H0)) (Pts_part_lemma a b Hab n P g gP i0 (RS'_Hsep_S i i0 Hi H0)))[*] (P (S i0) (RS'_Hsep_S i i0 Hi H0)[-]P i0 (RS'_Hsep i i0 Hi H0))) (fun _ : pred (sep__part_fun (S i) Hi) < i0 => [0]) (le_lt_dec i0 (pred (sep__part_fun (S i) Hi)))) (fun _ : i0 < sep__part_fun i (Nat.lt_le_incl i m Hi) => [0]) (le_lt_dec (sep__part_fun i (Nat.lt_le_incl i m Hi)) i0)) (h := part_tot_nat_fun _ _ (fun (i : nat) (H : i < n) => F (g i H) just1[*](P _ H[-]P _ (Nat.lt_le_incl _ _ H)))). apply sep__part_fun_0. intros; apply sep__part_fun_wd; auto. intros; apply sep__part_fun_mon; auto. intros. elim le_lt_dec; intro; simpl in |- *. elim le_lt_dec; intro; simpl in |- *. unfold part_tot_nat_fun in |- *. elim (le_lt_dec n j); intro; simpl in |- *. exfalso. apply Nat.le_ngt with n j. assumption. apply Nat.lt_le_trans with (sep__part_fun (S i) Hi''). assumption. apply sep__part_fun_bnd. apply mult_wd; algebra. apply cg_minus_wd; apply prf1; auto. exfalso. apply Nat.le_ngt with (sep__part_fun i Hi') j. assumption. cut (sep__part_fun i Hi' = sep__part_fun i (Nat.lt_le_incl _ _ Hi)); [ intro | apply sep__part_fun_wd; auto ]. rewrite H1; assumption. exfalso. apply Nat.le_ngt with (S j) (sep__part_fun (S i) Hi). cut (sep__part_fun (S i) Hi = sep__part_fun (S i) Hi''); [ intro | apply sep__part_fun_wd; auto ]. rewrite H1; apply H0. rewrite <- (Nat.lt_succ_pred (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) (sep__part_fun (S i) Hi)) . auto with arith. apply sep__part_fun_mon; apply Nat.lt_succ_diag_r. intros; symmetry in |- *; apply sep__part_fun_m. apply Sumx_wd; intros. unfold part_tot_nat_fun in |- *. elim (le_lt_dec n i); intro; simpl in |- *. exfalso; apply Nat.le_ngt with n i; auto. apply mult_wd; algebra. apply cg_minus_wd; apply prf1; auto. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)