proposition: Lemma Iu1: forall a b, ex_RInt (fun u => u1 u) a b.
proof: Proof. intros a b. apply continuity_implies_ex_Rint. apply Cu1. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Rcomplements Derive RInt Hierarchy Derive_2d AutoDerive)