proposition: Lemma compact_in_interval_y_lft : forall I pI x y Hx Hy H H', Lend (I:=compact_in_interval2 I pI x y Hx Hy) H [<=] Lend (I:=compact_in_interval I pI y Hy) H'.
proof: Proof. intros [| c| c| c| c| c c0| c c0| c c0| c c0]; simpl in |- *; intros; try apply minus_resp_leEq; try apply Min_leEq_rht; try apply leEq_reflexive; (rstepl (c[+] (Min x y[-]c) [/]TwoNZ); rstepr (c[+] (y[-]c) [/]TwoNZ); apply plus_resp_leEq_lft; apply div_resp_leEq; [ apply pos_two | apply minus_resp_leEq; apply Min_leEq_rht ]). Qed.
imports: CoRN.ftc.NthDerivative