proposition: Lemma RInt_helper : forall f u v i, (i <> Inan -> exists I : R, is_RInt f u v I /\ contains i (Xreal I)) -> (i <> Inan -> ex_RInt f u v) /\ contains i (Xreal (RInt f u v)).
proof: Proof. intros f u v [|il iu]. easy. intros [I [H1 H2]]. easy. split. intros _. now exists I. apply eq_ind with (1 := H2). apply f_equal, eq_sym. now apply is_RInt_unique. Qed.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority