proposition: Lemma sep__part_Sum3 : AbsIR (Partition_Sum gP incF[-]Partition_Sum sep__part_pts_in_Partition incF)[=] AbsIR (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[-]F (sep__part_pts i Hi) just2)[*] (P _ (RS'_Hsep_S _ _ _ Hj')[-]P _ (RS'_Hsep _ _ _ Hj'))))).
proof: Proof. apply AbsIR_wd. apply eq_transitive_unfolded with (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')))[-] F (sep__part_pts i Hi) just2[*] Sum2 (fun (j : nat) (Hj : sep__part_fun i (Nat.lt_le_incl _ _ Hi) <= j) (Hj' : j <= pred (sep__part_fun (S i) Hi)) => P _ (RS'_Hsep_S _ _ _ Hj')[-]P _ (RS'_Hsep _ _ _ Hj')))). eapply eq_transitive_unfolded. 2: apply Sumx_minus_Sumx with (f := 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')))) (g := fun (i : nat) (Hi : i < m) => F (sep__part_pts i Hi) just2[*] Sum2 (fun (j : nat) (Hj : sep__part_fun i (Nat.lt_le_incl _ _ Hi) <= j) (Hj' : j <= pred (sep__part_fun (S i) Hi)) => P _ (RS'_Hsep_S _ _ _ Hj')[-]P _ (RS'_Hsep _ _ _ Hj'))). apply cg_minus_wd. apply sep__part_Sum2. unfold Partition_Sum in |- *; apply Sumx_wd; intros. apply mult_wdr. apply eq_symmetric_unfolded; apply sep__part_suRS'_m1. apply Sumx_wd; intros i Hi. apply eq_transitive_unfolded with (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')))[-] 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 (sep__part_pts i Hi) just2[*] (P _ (RS'_Hsep_S _ _ _ Hj')[-]P _ (RS'_Hsep _ _ _ Hj')))). apply cg_minus_wd. algebra. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply Sum2_comm_scal'. algebra. rewrite (Nat.lt_succ_pred (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) (sep__part_fun (S i) Hi) (sep__part_fun_mon _ _ _ _ (Nat.lt_succ_diag_r i))). apply Nat.lt_le_incl; apply sep__part_fun_mon; apply Nat.lt_succ_diag_r. eapply eq_transitive_unfolded. apply Sum2_minus_Sum2. rewrite (Nat.lt_succ_pred (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) (sep__part_fun (S i) Hi) (sep__part_fun_mon _ _ _ _ (Nat.lt_succ_diag_r i))). apply Nat.lt_le_incl; apply sep__part_fun_mon; apply Nat.lt_succ_diag_r. apply Sum2_wd; intros. rewrite (Nat.lt_succ_pred (sep__part_fun i (Nat.lt_le_incl _ _ Hi)) (sep__part_fun (S i) Hi) (sep__part_fun_mon _ _ _ _ (Nat.lt_succ_diag_r i))). apply Nat.lt_le_incl; apply sep__part_fun_mon; apply Nat.lt_succ_diag_r. algebra. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions Coq(Lia)