proposition: Lemma Derivative_imp_resp_less : 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 a b) 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. apply shift_zero_less_minus'. cut (Continuous_I (Min_leEq_Max a b) 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 ]. elim (Law_of_the_Mean _ _ _ _ derF a b) with (e := (glb_funct _ _ _ _ H[*] (b[-]a)) [/]TwoNZ); auto. intros x H1 H2. apply less_leEq_trans with (F' x (contin_imp_inc _ _ _ _ H x H1) [*] (b[-]a) [-] (glb_funct _ _ _ _ H[*] (b[-]a)) [/]TwoNZ). rstepr ((F' x (contin_imp_inc _ _ _ _ H x H1) [-]glb_funct _ _ _ _ H [/]TwoNZ) [*] (b[-]a)). apply mult_resp_pos. apply shift_less_minus; astepl (glb_funct _ _ _ _ H [/]TwoNZ). eapply less_leEq_trans. apply pos_div_two'; auto. apply glb_prop. auto. apply shift_less_minus; astepl a; auto. apply shift_minus_leEq; apply shift_leEq_plus'. rstepl ( [--] (Part _ _ Hb[-]Part _ _ Ha[-] Part _ _ (contin_imp_inc _ _ _ _ H _ H1) [*] (b[-]a))). eapply leEq_transitive. apply inv_leEq_AbsIR. apply H2. apply pos_div_two; apply mult_resp_pos; auto. apply shift_less_minus; astepl a; auto. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3