proposition: Lemma third_refinement_lemma : AbsIR (Partition_Sum HfP incF[-]Partition_Sum HfR incF) [<=] e[*] (b[-]a) [+]e'[*] (b[-]a) [+]beta.
proof: Proof. apply leEq_wdl with (AbsIR (Partition_Sum HfP incF[-]Partition_Sum RL_fP'_in_P' incF[+] (Partition_Sum RL_fP'_in_P' incF[-]Partition_Sum RL_fQ_in_Q incF) [+] (Partition_Sum RL_fQ_in_Q incF[-]Partition_Sum RL_fR'_in_R' incF) [+] (Partition_Sum RL_fR'_in_R' incF[-]Partition_Sum HfR incF))). apply leEq_wdr with (alpha[+]alpha[+] (e[*] (b[-]a) [+]e'[*] (b[-]a)) [+]alpha). 2: unfold alpha in |- *; rational. eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. apply RL_P'_P_sum. apply RL_Q_P'_sum. 2: eapply leEq_wdl. 3: apply AbsIR_minus. 2: apply RL_R'_R_sum. 2: apply AbsIR_wd; rational. eapply second_refinement_lemma with (Q := Separated_Refinement _ _ _ _ _ _ _ RL_Q_sep) (He := He) (He' := He'). apply Separated_Refinement_lft. apply Separated_Refinement_rht. apply RL_Q_Mesh. apply less_leEq; apply RL_R'_Mesh. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef