proposition: Lemma refinement_lemma : AbsIR (Partition_Sum HfP incF[-]Partition_Sum HfR incF) [<=] e[*] (b[-]a) [+]e'[*] (b[-]a).
proof: Proof. cut ([0] [<] Min d d'). intro H; elim (less_cotransitive_unfolded _ _ _ H (b[-]a)); intro. astepr (e[*] (b[-]a) [+]e'[*] (b[-]a) [+][0]). apply shift_leEq_plus'. apply approach_zero_weak. intros beta Hbeta. apply shift_minus_leEq. astepr (e[*] (b[-]a) [+]e'[*] (b[-]a) [+]beta). apply third_refinement_lemma with (He := He) (He' := He'); try assumption. astepl ([0][+]a); apply shift_plus_less; assumption. apply fourth_refinement_lemma with He He'. assumption. apply less_Min. unfold d in |- *; apply proj2a_sig2T. unfold d' in |- *; apply proj2a_sig2T. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef