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 b a) F' contF') -> forall Ha Hb, F a Ha [#] F b Hb -> F a Ha [<] F b Hb.
proof: Proof. intros J pJ a b F F' H H0 H1 H2 H3 Ha Hb H4. elim (ap_imp_less _ _ _ H4); intro; auto. exfalso. apply less_irreflexive_unfolded with (x := F a Ha). apply leEq_less_trans with (F b Hb); auto. apply Derivative_imp_resp_leEq with J pJ F'; auto. apply less_leEq; auto. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3