proposition: Lemma C_RInt_scal_R (f : R -> C) (a b : R) (k : R) : C_RInt (fun t => scal k (f t)) a b = scal k (C_RInt f a b).
proof: Proof. apply injective_projections ; simpl ; apply RInt_scal. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)