proposition: Lemma diff_refining_aux_1 : forall prec f f' xi yi' m mi ymi, Xderive f f' -> contains (I.convert mi) (Xreal m) -> contains (I.convert xi) (Xreal m) -> contains (I.convert ymi) (f (Xreal m)) -> (forall x, contains (I.convert xi) x -> contains (I.convert yi') (f' x)) -> forall x, contains (I.convert xi) x -> contains (I.convert (I.add prec ymi (I.mul prec (I.sub prec xi mi) yi'))) (f x).
proof: Proof. intros prec f f' xi yi' m mi ymi Hd Hxm Hm Hym Hy' x Hx. case_eq (I.convert yi'). intro Hyn'. rewrite I.add_propagate_r. easy. now apply I.mul_propagate_r. intros yl' yu' Hyi'. destruct x as [|x]. case_eq (I.convert xi). intros Hxi. generalize (Hy' _ Hx). rewrite Hyi'. generalize (Hd Xnan). unfold Xderive_pt. case (f' Xnan). intros _ H. elim H. intros _ H _. elim H. intros xl xu Hxi. rewrite Hxi in Hx. elim Hx. set (Pxi := fun x => contains (I.convert xi) (Xreal x)). assert (H': forall c, Pxi c -> f' (Xreal c) <> Xnan). intros c Hc H. generalize (Hy' (Xreal c) Hc). rewrite H Hyi'. intro H0. elim H0. destruct (Xderive_MVT _ _ Hd Pxi (contains_connected _) H' _ Hm _ Hx) as (c, (Hc1, Hc2)). rewrite Hc2. apply I.add_correct. exact Hym. rewrite Xmul_comm. apply I.mul_correct. now apply I.sub_correct. apply Hy'. exact Hc1. 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