proposition: Lemma partition_Sum_conv_integral : AbsIR (Partition_Sum HfP incF[-]integral) [<=] e[*] (b[-]a).
proof: Proof. apply leEq_wdl with (AbsIR (Partition_Sum HfP (contin_imp_inc _ _ _ _ contF) [-]integral)). Proof. apply leEq_wdl with (AbsIR (Lim (Cauchy_const (Partition_Sum HfP (contin_imp_inc _ _ _ _ contF))) [-] integral)). 2: apply AbsIR_wd; apply cg_minus_wd; [ apply eq_symmetric_unfolded; apply Lim_const | algebra ]. unfold integral in |- *. apply leEq_wdl with (AbsIR (Lim (Build_CauchySeq _ _ (Cauchy_minus (Cauchy_const (Partition_Sum HfP (contin_imp_inc _ _ _ _ contF))) (Build_CauchySeq _ _ Cauchy_Darboux_Seq))))). 2: apply AbsIR_wd; apply Lim_minus. eapply leEq_wdl. 2: apply Lim_abs. astepr ([0][+]e[*] (b[-]a)); apply shift_leEq_plus; apply approach_zero_weak. intros e' He'. set (ee := e'[/] _[//]max_one_ap_zero (b[-]a)) in *. apply leEq_transitive with (ee[*] (b[-]a)). cut ([0] [<] ee). intro Hee. set (d' := proj1_sig2T _ _ _ (contF' _ Hee)) in *. generalize (proj2b_sig2T _ _ _ (contF' _ Hee)); generalize (proj2a_sig2T _ _ _ (contF' _ Hee)); fold d' in |- *; intros Hd' Hd'0. elim (Archimedes (b[-]a[/] _[//]pos_ap_zero _ _ Hd')); intros k Hk. apply shift_minus_leEq. eapply leEq_wdr. 2: apply cag_commutes_unfolded. apply str_seq_leEq_so_Lim_leEq. exists k; simpl in |- *; intros. unfold integral_seq, Even_Partition_Sum in |- *. apply refinement_lemma with contF He Hee. assumption. fold d' in |- *. eapply less_wdl. 2: apply eq_symmetric_unfolded; apply even_partition_Mesh. apply shift_div_less. apply pos_nring_S. apply shift_less_mult' with (pos_ap_zero _ _ Hd'). assumption. apply leEq_less_trans with (nring (R:=IR) k). assumption. apply nring_less; auto with arith. assumption. red in |- *; do 3 intro. rewrite H0; intros; simpl in |- *; algebra. unfold ee in |- *; apply div_resp_pos. apply pos_max_one. assumption. unfold ee in |- *. rstepl (e'[*] (b[-]a[/] _[//]max_one_ap_zero (b[-]a))). rstepr (e'[*][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; assumption. apply AbsIR_wd; apply cg_minus_wd. unfold Partition_Sum in |- *. apply Sumx_wd; intros. algebra. algebra. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)