proposition: Theorem contains_RInt_valid : forall f u v i, valid (at_point u) (at_point v) f IBu IBv i -> contains (I.convert i) (Xreal (RInt f u v)).
proof: Proof. intros f u v i [H1 H2]. destruct (I.convert i) as [|il iu]. easy. rewrite <- RInt_gen_at_point. exact H2. apply ex_RInt_gen_at_point. now apply H1. Qed.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority