proposition: Lemma diff_refining_aux_2 : forall f f' xi m ymi, Xderive f f' -> contains xi (Xreal m) -> contains ymi (f (Xreal m)) -> (forall x, contains xi x -> contains (Ibnd (Xreal 0) (Xreal 0)) (f' x)) -> forall x, contains xi x -> contains ymi (f x).
proof: Proof. intros f f' xi m ymi Hd Hm Hym Hy'. destruct xi as [|xl xu]. apply False_ind. generalize (Hy' Xnan I) (Hd Xnan). now case (f' (Xnan)). intros [|x] Hx. elim Hx. set (Pxi := fun x => contains (Ibnd xl xu) (Xreal x)). assert (H': forall c, Pxi c -> f' (Xreal c) <> Xnan). intros c Hc H. generalize (Hy' (Xreal c) Hc). now rewrite H. destruct (Xderive_MVT _ _ Hd Pxi (contains_connected _) H' _ Hm _ Hx) as (c, (Hc1, Hc2)). rewrite Hc2. replace (f' (Xreal c)) with (Xreal 0). simpl. rewrite Rmult_0_l. rewrite Xadd_0_r. exact Hym. generalize (Hy' (Xreal c) Hc1). destruct (f' (Xreal c)) as [|y]. intro H. elim H. intros (H3,H4). apply f_equal. now apply Rle_antisym. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog