proposition: Lemma C_RInt_scal (f : R -> C) (k : C) (a b : R) : ex_RInt f a b -> C_RInt (fun t => k * f t) a b = k * C_RInt f a b.
proof: Proof. intros Hf. apply is_C_RInt_unique. apply is_C_RInt_scal. by apply C_RInt_correct. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)