proposition: Theorem valid_at_point : forall f u v fi ui vi, contains (I.convert ui) (Xreal u) -> contains (I.convert vi) (Xreal v) -> (forall ui' vi' u' v', contains (I.convert ui') (Xreal u') -> contains (I.convert vi') (Xreal v') -> (I.convert (fi ui' vi') <> Inan -> ex_RInt f u' v') /\ contains (I.convert (fi ui' vi')) (Xreal (RInt f u' v'))) -> forall u' v', let cb := fun x => match x with IBu => ui | IBv => vi | IBp x => I.singleton x end in valid (at_point u) (at_point v) f u' v' (fi (cb u') (cb v')).
proof: Proof. intros f u v fi ui vi Hu Hv Hf u' v' cb. unfold valid. set (cb' p := match p with IBu => u | IBv => v | IBp x => proj_val (I.F.convert x) end). assert (H1: forall p, at_point (cb' p) = convert (at_point u) (at_point v) p). now intros [| |p]. assert (H2: forall p, contains (I.convert (cb p)) (Xreal (cb' p))). intros [| |p]. exact Hu. exact Hv. apply I.singleton_correct. rewrite <- 2!H1. destruct (Hf (cb u') (cb v') (cb' u') (cb' v') (H2 u') (H2 v')) as [H3 H4]. destruct (I.convert (fi (cb u') (cb v'))) as [|il iu] eqn:E. easy. split. intros _. apply <- (ex_RInt_gen_at_point f). now apply H3. rewrite RInt_gen_at_point. exact H4. now apply H3. Qed.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority