proposition: Theorem valid_at_mixed : forall f u v (Fv: ProperFilter v) fi1 fi2 ui, contains (I.convert ui) (Xreal u) -> (forall ui' vi' u' v', contains (I.convert ui') (Xreal u') -> contains (I.convert vi') (Xreal v') -> (I.convert (fi1 ui' vi') <> Inan -> ex_RInt f u' v') /\ contains (I.convert (fi1 ui' vi')) (Xreal (RInt f u' v'))) -> (forall ui' u', contains (I.convert ui') (Xreal u') -> (I.convert (fi2 ui') <> Inan -> ex_RInt_gen f (at_point u') v) /\ contains (I.convert (fi2 ui')) (Xreal (RInt_gen f (at_point u') v))) -> forall u' v', valid (at_point u) v f u' v' (match u', v' with | IBu, IBp xu => fi1 ui (I.singleton xu) | IBp xl, IBp xu => fi1 (I.singleton xl) (I.singleton xu) | IBu, IBv => fi2 ui | IBp xl, IBv => fi2 (I.singleton xl) | _, _ => I.nai end).
proof: Proof. intros f u v Fv fi1 fi2 ui Hu Hf1 Hf2 u' v'. unfold valid. destruct u' as [| |ur] ; destruct v' as [| |vr] ; try (rewrite I.nai_correct ; apply valid_Inan). - now apply Hf2. - destruct (Hf1 ui _ u _ Hu (I.singleton_correct vr)) as [H2 H3]. destruct (I.convert (fi1 ui (I.singleton vr))) as [|il iu] eqn:E. easy. split. intros _. apply <- (ex_RInt_gen_at_point f). now apply H2. simpl convert. rewrite RInt_gen_at_point. apply H3. now apply H2. - destruct (Hf2 _ _ (I.singleton_correct ur)) as [H2 H3]. destruct (I.convert (fi2 (I.singleton ur))) as [|il iu] eqn:E. easy. split. intros _. now apply H2. apply H3. - destruct (Hf1 _ _ _ _ (I.singleton_correct ur) (I.singleton_correct vr)) as [H2 H3]. destruct (I.convert (fi1 (I.singleton ur) (I.singleton vr))) as [|il iu] eqn:E. easy. split. intros _. apply <- (ex_RInt_gen_at_point f). now apply H2. simpl convert. rewrite RInt_gen_at_point. apply H3. now apply H2. Qed.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority