proposition: Lemma sep__sep_Sum : AbsIR (Partition_Sum gP incF[-]Partition_Sum sep__sep_points_lemma incF)[<=] alpha.
proof: Proof. unfold Partition_Sum in |- *; simpl in |- *. rstepr (alpha [/]TwoNZ[+]alpha [/]TwoNZ). apply leEq_transitive with (e[*](b[-]a)[+]nring n[*]M[*]delta). apply leEq_wdr with (e[*] Sumx (fun (i : nat) (Hi : i < n) => P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi))[+] Sumx (fun (i : nat) (Hi : i < n) => M[*]delta)). apply leEq_transitive with (Sumx (fun (i : nat) (Hi : i < n) => AbsIR (F (g i Hi) just1[-]F (sep__sep_points i Hi) just2)[*] (P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi)))[+] Sumx (fun (i : nat) (Hi : i < n) => AbsIR (F (sep__sep_points i Hi) just2)[*] (AbsIR (sep__sep_fun _ Hi[-]P _ Hi)[+] AbsIR (P _ (Nat.lt_le_incl _ _ Hi)[-]sep__sep_fun _ (Nat.lt_le_incl _ _ Hi))))). apply leEq_transitive with (AbsIR (Sumx (fun (i : nat) (Hi : i < n) => F (g i Hi) just1[*](P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi))[-] F (sep__sep_points i Hi) just2[*] (P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi))))[+] AbsIR (Sumx (fun (i : nat) (Hi : i < n) => F (sep__sep_points i Hi) just2[*] (sep__sep_fun _ Hi[-]P _ Hi[+] (P _ (Nat.lt_le_incl _ _ Hi)[-]sep__sep_fun _ (Nat.lt_le_incl _ _ Hi)))))). eapply leEq_wdl. apply triangle_IR_minus. apply eq_symmetric_unfolded. apply AbsIR_wd. eapply eq_transitive_unfolded. apply Sumx_minus_Sumx. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply Sumx_minus_Sumx. apply Sumx_wd; intros. astepl (F (g i H) just1[*](P _ H[-]P _ (Nat.lt_le_incl _ _ H))[-] F (sep__sep_points i H) just2[*] (sep__sep_fun _ H[-]sep__sep_fun _ (Nat.lt_le_incl _ _ H))). rational. apply plus_resp_leEq_both. eapply leEq_wdr. apply triangle_SumxIR. apply Sumx_wd; intros. apply eq_transitive_unfolded with (AbsIR (F (g i H) just1[-]F (sep__sep_points i H) just2)[*] AbsIR (P _ H[-]P _ (Nat.lt_le_incl _ _ H))). eapply eq_transitive_unfolded. 2: apply AbsIR_resp_mult. apply AbsIR_wd; algebra. apply mult_wdr. apply AbsIR_eq_x. apply shift_leEq_minus; astepl (P i (Nat.lt_le_incl _ _ H)); apply prf2. eapply leEq_transitive. apply triangle_SumxIR. apply Sumx_resp_leEq; intros. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_lft. apply triangle_IR. apply AbsIR_nonneg. apply plus_resp_leEq_both. eapply leEq_wdr. 2: apply Sumx_comm_scal'. apply Sumx_resp_leEq; intros. apply mult_resp_leEq_rht. apply sep__sep_aux. apply shift_leEq_minus; astepl (P i (Nat.lt_le_incl _ _ H)); apply prf2. apply Sumx_resp_leEq; intros. apply mult_resp_leEq_both. apply AbsIR_nonneg. astepl (ZeroR[+][0]); apply plus_resp_leEq_both; apply AbsIR_nonneg. unfold I, M in |- *; apply norm_bnd_AbsIR. apply Pts_part_lemma with n sep__sep_part; apply sep__sep_points_lemma. rstepr (delta [/]TwoNZ[+]delta [/]TwoNZ). apply plus_resp_leEq_both. apply sep__sep_fun_delta. eapply leEq_wdl. 2: apply AbsIR_minus. apply sep__sep_fun_delta. apply bin_op_wd_unfolded. apply mult_wdr. eapply eq_transitive_unfolded. apply Mengolli_Sum with (f := fun (i : nat) (Hi : i <= n) => P i Hi). red in |- *; intros; apply prf1; auto. intros; algebra. apply cg_minus_wd. apply finish. apply start. astepr (nring n[*](M[*]delta)); apply sumx_const. apply plus_resp_leEq_both. unfold e in |- *. apply leEq_wdl with (alpha [/]TwoNZ[*](b[-]a[/] _[//]max_one_ap_zero (b[-]a))). rstepr (alpha [/]TwoNZ[*][1]). apply mult_resp_leEq_lft. apply shift_div_leEq. apply pos_max_one. astepr (Max (b[-]a) [1]); apply lft_leEq_Max. apply less_leEq; apply pos_div_two; assumption. simpl in |- *; rational. apply leEq_transitive with (Max (nring n[*]M) [1][*]delta). apply mult_resp_leEq_rht. apply lft_leEq_Max. apply less_leEq; apply RS_delta_pos. apply shift_mult_leEq' with (max_one_ap_zero (nring n[*]M)). apply pos_max_one. unfold delta in |- *. eapply leEq_transitive. apply Min_leEq_rht. apply Min_leEq_lft. Qed.
imports: CoRN.ftc.COrdLemmas CoRN.ftc.Partitions