proposition: Lemma fourth_refinement_lemma : AbsIR (Partition_Sum HfP incF[-]Partition_Sum HfR incF) [<=] e[*] (b[-]a) [+]e'[*] (b[-]a).
proof: Proof. generalize (proj2b_sig2T _ _ _ (contF' e He)); generalize (proj2a_sig2T _ _ _ (contF' e He)); fold d in |- *; intros Hd Hdd. generalize (proj2b_sig2T _ _ _ (contF' e' He')); generalize (proj2a_sig2T _ _ _ (contF' e' He')); fold d' in |- *; intros Hd' Hdd'. apply leEq_wdl with (AbsIR (Fa[*] (b[-]a) [-] Sumx (fun (i : nat) (Hi : i < n) => (Fa[-]Part F (fP i Hi) (just HfP)) [*] (P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi))) [-] (Fa[*] (b[-]a) [-] Sumx (fun (j : nat) (Hj : j < m) => (Fa[-]Part F (fR j Hj) (just HfR)) [*] (R _ Hj[-]R _ (Nat.lt_le_incl _ _ Hj)))))). 2: apply AbsIR_wd; apply eq_symmetric_unfolded. 2: apply cg_minus_wd; apply RL_sum_lemma_aux. apply leEq_wdl with (AbsIR (Sumx (fun (j : nat) (Hj : j < m) => (Fa[-]Part F (fR j Hj) (just HfR)) [*] (R _ Hj[-]R _ (Nat.lt_le_incl _ _ Hj))) [-] Sumx (fun (i : nat) (Hi : i < n) => (Fa[-]Part F (fP i Hi) (just HfP)) [*] (P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi))))). 2: apply AbsIR_wd; rational. rstepr (e'[*] (b[-]a) [+]e[*] (b[-]a)). eapply leEq_transitive. apply triangle_IR_minus. apply plus_resp_leEq_both. eapply leEq_transitive. apply triangle_SumxIR. apply leEq_wdr with (Sumx (fun (i : nat) (Hi : i < m) => e'[*] (R _ Hi[-]R _ (Nat.lt_le_incl _ _ Hi)))). apply Sumx_resp_leEq; intros. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try apply AbsIR_nonneg. unfold Fa in |- *; apply Hdd'; unfold I in |- *. apply compact_inc_lft. apply Pts_part_lemma with m R; assumption. apply leEq_transitive with (AbsIR (b[-]a)). apply compact_elements with Hab. apply compact_inc_lft. apply Pts_part_lemma with m R; assumption. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl a; assumption. eapply leEq_transitive. apply less_leEq; apply Hab'. apply Min_leEq_rht. apply eq_imp_leEq; apply AbsIR_eq_x. apply shift_leEq_minus; astepl (R i (Nat.lt_le_incl _ _ H)); apply prf2. eapply eq_transitive_unfolded. apply Sumx_comm_scal' with (f := fun (i : nat) (Hi : i < m) => R _ Hi[-]R _ (Nat.lt_le_incl _ _ Hi)). apply mult_wdr. eapply eq_transitive_unfolded. apply Mengolli_Sum with (f := fun (i : nat) (Hi : i <= m) => R i Hi). red in |- *; intros. apply prf1; auto. intros; algebra. apply cg_minus_wd; [ apply finish | apply start ]. eapply leEq_transitive. apply triangle_SumxIR. apply leEq_wdr with (Sumx (fun (i : nat) (Hi : i < n) => e[*] (P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi)))). apply Sumx_resp_leEq; intros. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_both; try apply AbsIR_nonneg. unfold Fa in |- *; apply Hdd; unfold I in |- *. apply compact_inc_lft. apply Pts_part_lemma with n P; assumption. apply leEq_transitive with (AbsIR (b[-]a)). apply compact_elements with Hab. apply compact_inc_lft. apply Pts_part_lemma with n P; assumption. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. 2: apply shift_leEq_minus; astepl a; assumption. eapply leEq_transitive. apply less_leEq; apply Hab'. apply Min_leEq_lft. apply eq_imp_leEq; apply AbsIR_eq_x. apply shift_leEq_minus; astepl (P i (Nat.lt_le_incl _ _ H)); apply prf2. eapply eq_transitive_unfolded. apply Sumx_comm_scal' with (f := fun (i : nat) (Hi : i < n) => P _ Hi[-]P _ (Nat.lt_le_incl _ _ Hi)). 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 ]. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef