proposition: Lemma diff_refining_aux_0 : forall f f' xi yi', Xderive f f' -> I.sign_large yi' <> Xund -> (forall x, contains xi x -> contains (I.convert yi') (f' x)) -> forall x, contains xi x -> x = Xreal (proj_val x) /\ forall v, f x = Xreal (proj_fun v f (proj_val x)) /\ f' x = Xreal (proj_fun v f' (proj_val x)).
proof: Proof. intros f f' xi yi' Hd Hs Hy' x Hx. case_eq (f' x). intros Hnf'. generalize (Hy' _ Hx). rewrite Hnf'. intros Hny'. apply False_ind. generalize (I.sign_large_correct yi'). destruct (I.sign_large yi') ; intros H. generalize (H _ Hny'). discriminate. destruct (H _ Hny') as (H0, _). discriminate H0. destruct (H _ Hny') as (H0, _). discriminate H0. now elim Hs. intros ry' Hrf'. generalize (Hd x). destruct x as [|x]. rewrite Hrf'. now intro H. rewrite Hrf'. unfold Xderive_pt. case_eq (f (Xreal x)). now intros _ H. intros ry Hrf _. repeat split. unfold proj_fun, proj_val. now rewrite Hrf. unfold proj_fun, proj_val. now rewrite Hrf'. 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