proposition: Lemma compact_in_interval_x_rht : forall I pI x y Hx Hy H H', Rend (I:=compact_in_interval I pI x Hx) H [<=] Rend (I:=compact_in_interval2 I pI x y Hx Hy) H'.
proof: Proof. intros [| c| c| c| c| c c0| c c0| c c0| c c0]; simpl in |- *; intros; try apply plus_resp_leEq; try apply lft_leEq_Max; try apply leEq_reflexive; (rstepl (c0[-] (c0[-]x) [/]TwoNZ); rstepr (c0[-] (c0[-]Max x y) [/]TwoNZ); unfold cg_minus in |- *; apply plus_resp_leEq_lft; apply inv_resp_leEq; apply div_resp_leEq; [ apply pos_two | apply plus_resp_leEq_lft; apply inv_resp_leEq; apply lft_leEq_Max ]). Qed.
imports: CoRN.ftc.NthDerivative