proposition: Lemma is_RInt_scal_derive_l : forall (f : R -> R) (g : R -> V) (f' : R -> R) (g' : R -> V) (a b : R) (l : V), (forall t, Rmin a b <= t <= Rmax a b -> is_derive f t (f' t)) -> (forall t, Rmin a b <= t <= Rmax a b -> is_derive g t (g' t)) -> (forall t, Rmin a b <= t <= Rmax a b -> continuous f' t) -> (forall t, Rmin a b <= t <= Rmax a b -> continuous g' t) -> is_RInt (fun t => scal (f t) (g' t)) a b l -> is_RInt (fun t => scal (f' t) (g t)) a b (minus (minus (scal (f b) (g b)) (scal (f a) (g a))) l).
proof: Proof. intros f g f' g' a b l Df Dg Cf' Cg' If'g. apply (is_RInt_ext (fun t => minus (plus (scal (f' t) (g t)) (scal (f t) (g' t))) (scal (f t) (g' t)))). intros x H. by rewrite /minus -plus_assoc plus_opp_r plus_zero_r. apply is_RInt_minus with (2 := If'g). exact: is_RInt_scal_derive. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(eqtype seq) Markov Rcomplements Rbar Lub Lim_seq Derive SF_seq Continuity Hierarchy Seq_fct RInt PSeries