proposition: Lemma C_RInt_ext (f g : R -> C) (a b : R) : (forall x, Rmin a b <= x <= Rmax a b -> g x = f x) -> C_RInt g a b = C_RInt f a b.
proof: Proof. intros Heq. apply injective_projections ; simpl ; apply RInt_ext => x Hx ; by rewrite Heq. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)