proposition: Lemma second_refinement_lemma : AbsIR (Partition_Sum HfP incF[-]Partition_Sum HfR incF) [<=] e[*] (b[-]a) [+]e'[*] (b[-]a).
proof: Proof. set (HfQ := Partition_imp_points_1 _ _ _ _ Q) in *. set (H' := Partition_imp_points_2 _ _ _ _ Q) in *. apply leEq_wdl with (AbsIR (Partition_Sum HfP incF[-]Partition_Sum HfQ incF[+] (Partition_Sum HfQ incF[-]Partition_Sum HfR incF))). 2: apply AbsIR_wd; rational. eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. apply first_refinement_lemma with He; assumption. eapply leEq_wdl. 2: apply AbsIR_minus. apply first_refinement_lemma with He'; assumption. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef