proposition: Theorem valid_at_mixed' : forall f u v (Fu: ProperFilter u) fi1 fi2 vi, 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 (fi1 ui' vi') <> Inan -> ex_RInt f u' v') /\ contains (I.convert (fi1 ui' vi')) (Xreal (RInt f u' v'))) -> (forall vi' v', contains (I.convert vi') (Xreal v') -> (I.convert (fi2 vi') <> Inan -> ex_RInt_gen f u (at_point v')) /\ contains (I.convert (fi2 vi')) (Xreal (RInt_gen f u (at_point v')))) -> forall u' v', valid u (at_point v) f u' v' (match u', v' with | IBu, IBp xu => fi2 (I.singleton xu) | IBp xl, IBp xu => fi1 (I.singleton xl) (I.singleton xu) | IBu, IBv => fi2 vi | IBp xl, IBv => fi1 (I.singleton xl) vi | _, _ => I.nai end).
proof: Proof. intros f u v Fu fi1 fi2 vi Hv 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 (Hf2 _ _ (I.singleton_correct vr)) as [H2 H3]. destruct (I.convert (fi2 (I.singleton vr))) as [|il iu] eqn:E. easy. split. intros _. now apply H2. apply H3. - destruct (Hf1 _ vi _ v (I.singleton_correct ur)) as [H2 H3]. apply Hv. destruct (I.convert (fi1 (I.singleton ur) vi)) 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 (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