proposition: Lemma RInt_gen_helper : forall f u v {Fu : ProperFilter' u} {Fv : ProperFilter' v} i, (i <> Inan -> exists I : R, is_RInt_gen f u v I /\ contains i (Xreal I)) -> (i <> Inan -> ex_RInt_gen f u v) /\ contains i (Xreal (RInt_gen f u v)).
proof: Proof. intros f u v Fu Fv [|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_gen_unique. Qed.
imports: Coq(BinPos Reals List) Coquelicot(Coquelicot) Coquelicot Xreal Interval Priority