proposition: Lemma C_RInt_correct (f : R -> C) (a b : R) : ex_RInt f a b -> is_RInt f a b (C_RInt f a b).
proof: Proof. case => l Hf. replace (C_RInt f a b) with l. by []. by apply sym_eq, is_C_RInt_unique. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)