proposition: Lemma integral_plus_integral : integral _ _ Hac _ Hac'[+]integral _ _ Hcb _ Hcb' [=] Integral _ Hab'.
proof: Proof. unfold integral at 1 2 in |- *. eapply eq_transitive_unfolded. apply eq_symmetric_unfolded; apply Lim_plus. apply cg_inv_unique_2. apply AbsIR_approach_zero. intros e' He'. set (e := e'[/] _[//]max_one_ap_zero (b[-]a)) in *. cut ([0] [<] e). intro He. set (d := proj1_sig2T _ _ _ (contin_prop _ _ _ _ Hab' e He)) in *. generalize (proj2b_sig2T _ _ _ (contin_prop _ _ _ _ Hab' e He)); generalize (proj2a_sig2T _ _ _ (contin_prop _ _ _ _ Hab' e He)). fold d in |- *; intros Hd Haux. clear Haux. apply leEq_transitive with (e[*] (b[-]a)). elim (Archimedes (b[-]c[/] _[//]pos_ap_zero _ _ Hd)); intros n1 Hn1. elim (Archimedes (c[-]a[/] _[//]pos_ap_zero _ _ Hd)); intros n2 Hn2. apply leEq_wdl with (Lim (Build_CauchySeq _ _ (Cauchy_abs (Build_CauchySeq _ _ (Cauchy_plus (Build_CauchySeq _ _ (Cauchy_plus (Build_CauchySeq _ _ (Cauchy_Darboux_Seq _ _ Hac _ Hac')) (Build_CauchySeq _ _ (Cauchy_Darboux_Seq _ _ Hcb _ Hcb')))) (Cauchy_const [--] (Integral _ Hab'))))))). apply str_seq_leEq_so_Lim_leEq. set (p := Nat.max n1 n2) in *; exists p; intros. astepl (AbsIR (integral_seq _ _ Hac _ Hac' i[+]integral_seq _ _ Hcb _ Hcb' i[-] Integral _ Hab')). unfold integral_seq, Even_Partition_Sum in |- *. set (EP1 := Even_Partition Hac (S i) (O_S i)) in *. set (EP2 := Even_Partition Hcb (S i) (O_S i)) in *. set (P := partition_join _ _ EP1 EP2) in *. cut (nat_less_n_fun (Partition_imp_points _ _ _ _ EP1)); [ intro | apply Partition_imp_points_2 ]. cut (nat_less_n_fun (Partition_imp_points _ _ _ _ EP2)); [ intro | apply Partition_imp_points_2 ]. apply leEq_wdl with (AbsIR (Partition_Sum (partition_join_Pts_in_partition _ _ _ _ _ (Partition_imp_points_1 _ _ _ _ EP1) H0 _ (Partition_imp_points_1 _ _ _ _ EP2) H1) (contin_imp_inc _ _ _ _ Hab') [-]Integral _ Hab')). apply partition_Sum_conv_integral with He; fold d in |- *. eapply leEq_less_trans. apply partition_join_mesh. apply Max_less. unfold EP1 in |- *; eapply less_wdl. 2: apply eq_symmetric_unfolded; apply even_partition_Mesh. apply swap_div with (pos_ap_zero _ _ Hd). apply pos_nring_S. assumption. apply leEq_less_trans with (nring (R:=IR) n2). assumption. apply nring_less. apply Nat.le_lt_trans with p. unfold p in |- *; apply Nat.le_max_r. auto with arith. unfold EP2 in |- *; eapply less_wdl. 2: apply eq_symmetric_unfolded; apply even_partition_Mesh. apply swap_div with (pos_ap_zero _ _ Hd). apply pos_nring_S. assumption. apply leEq_less_trans with (nring (R:=IR) n1). assumption. apply nring_less. apply Nat.le_lt_trans with p. unfold p in |- *; apply Nat.le_max_l. auto with arith. red in |- *; do 3 intro. rewrite H2; clear H2; intros. apply partition_join_Pts_wd; auto. apply AbsIR_wd. apply cg_minus_wd. 2: algebra. apply eq_symmetric_unfolded. unfold Partition_Sum in |- *; apply Sumx_weird_lemma. auto. red in |- *; do 3 intro. rewrite H2; clear H2; intros; algebra. red in |- *; do 3 intro. rewrite H2; clear H2; intros; algebra. red in |- *; do 3 intro. rewrite H2; clear H2; intros; algebra. Opaque Even_Partition. intros; apply mult_wd. apply pfwdef; unfold partition_join_pts in |- *. elim le_lt_dec; intro; simpl in |- *. elim le_lt_eq_dec; intro; simpl in |- *. apply Partition_imp_points_2; auto. exfalso; rewrite b0 in Hi; apply (Nat.lt_irrefl _ Hi). exfalso; apply Nat.le_ngt with i0 (S i); auto with arith. apply cg_minus_wd; simpl in |- *. apply eq_symmetric_unfolded; apply pjf_1. apply eq_symmetric_unfolded; apply pjf_1. intros; apply mult_wd. apply pfwdef; unfold Partition_imp_points in |- *. unfold partition_join_pts in |- *. elim le_lt_dec; intro; simpl in |- *. elim le_lt_eq_dec; intro; simpl in |- *. exfalso; apply Nat.nle_succ_diag_l with (S i); eapply Nat.le_trans. 2: apply a0. auto with arith. exfalso; apply Nat.lt_irrefl with (S i); pattern (S i) at 2 in |- *; rewrite <- b0; auto with arith. unfold Partition_imp_points in |- *; apply prf1. auto with arith. apply cg_minus_wd; simpl in |- *. apply eq_symmetric_unfolded; apply pjf_3; [ auto with arith | lia ]. apply eq_symmetric_unfolded; apply pjf_3; auto with arith. intro; apply x_mult_zero. astepr (c[-]c). apply cg_minus_wd. simpl in |- *; apply pjf_2'; auto. simpl in |- *; apply pjf_2; auto. eapply eq_transitive_unfolded. apply Lim_abs. apply AbsIR_wd. unfold cg_minus in |- *. eapply eq_transitive_unfolded. apply Lim_plus. apply bin_op_wd_unfolded. algebra. apply eq_symmetric_unfolded; apply Lim_const. unfold e in |- *. rstepl (e'[*] (b[-]a) [/] _[//]max_one_ap_zero (b[-]a)). apply shift_div_leEq. apply pos_max_one. apply mult_resp_leEq_lft. apply lft_leEq_Max. apply less_leEq; assumption. unfold e in |- *. apply div_resp_pos. apply pos_max_one. assumption. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)