proposition: Lemma is_C_RInt_scal f a b (k : C) l : is_RInt f a b l -> is_RInt (fun t => k * f t) a b (k * l).
proof: Proof. intros H. move: (is_RInt_fct_extend_fst _ _ _ _ H) => /= H1. move: (is_RInt_fct_extend_snd _ _ _ _ H) => /= {H} H2. apply is_RInt_fct_extend_pair ; simpl. by apply: is_RInt_minus ; apply: is_RInt_scal. by apply: is_RInt_plus ; apply: is_RInt_scal. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)