proposition: Lemma Derivative_imp_resp_leEq : forall J pJ a b F F', Derivative J pJ F F' -> a [<=] b -> J a -> J b -> (forall contF', [0] [<=] glb_funct _ _ (Min_leEq_Max b a) F' contF') -> forall Ha Hb, F a Ha [<=] F b Hb.
proof: Proof. intros J pJ a b F F' derF Hab HaJ HbJ Hglb Ha Hb. astepr ([0][+]Part _ _ Hb); apply shift_leEq_plus. cut (Continuous_I (Min_leEq_Max b a) F'). intro H. 2: apply included_imp_Continuous with J; [ apply Derivative_imp_Continuous' with pJ F | apply included_interval ]; auto. elim (glb_is_glb _ _ _ _ H). simpl in |- *; intros Hglb1 Hglb2. cut ([0] [<=] glb_funct _ _ _ _ H); [ intro H0 | auto ]. apply approach_zero_weak. intros. elim (Law_of_the_Mean _ _ _ _ derF b a) with (e := e); auto. intros x H2 H3. eapply leEq_transitive. 2: apply (H3 Hb Ha (contin_imp_inc _ _ _ _ H x H2)). eapply leEq_transitive. 2: apply leEq_AbsIR. rstepl (Part _ _ Ha[-]Part _ _ Hb[-][--][0]). unfold cg_minus at 1 3 in |- *; apply plus_resp_leEq_lft. apply inv_resp_leEq. rstepl ( [--] (Part _ _ (contin_imp_inc _ _ _ _ H _ H2) [*] (b[-]a))). apply inv_resp_leEq. apply mult_resp_nonneg. eapply leEq_transitive; [ apply H0 | apply Hglb1 ]. exists x. split. auto. split; algebra. apply (contin_imp_inc _ _ _ _ H); auto. apply shift_leEq_minus; astepl a; auto. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3