proposition: Lemma is_C_RInt_derive (f df : R -> C) (a b : R) : (forall x : R, Rmin a b <= x <= Rmax a b -> is_derive f x (df x)) -> (forall x : R, Rmin a b <= x <= Rmax a b -> continuous (U := C_R_NormedModule) df x) -> is_RInt df a b (f b - f a).
proof: Proof. intros. apply is_RInt_fct_extend_pair ; simpl. apply (is_RInt_derive (fun y => fst (f y)) (fun y => fst (df y))). intros x Hx. unfold is_derive. evar_last. apply (filterdiff_comp' f (@fst R R)). by apply H. apply filterdiff_linear, is_linear_fst. by simpl. intros x Hx. apply continuous_comp. by apply H0. apply continuous_fst. apply (is_RInt_derive (fun y => snd (f y)) (fun y => snd (df y))). intros x Hx. unfold is_derive. evar_last. apply (filterdiff_comp' f (@snd R R)). by apply H. apply filterdiff_linear, is_linear_snd. by simpl. intros x Hx. apply continuous_comp. by apply H0. apply continuous_snd. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)