proposition: Lemma Rint_parts : forall f g a b f' g' Ifg' If'g, a <= b -> (forall x : R, a <= x <= b -> derivable_pt_lim f x (f' x)) -> (forall x : R, a <= x <= b -> derivable_pt_lim g x (g' x)) -> (forall x : R, a <= x <= b -> continuity_pt f' x) -> (forall x : R, a <= x <= b -> continuity_pt g' x) -> Rint (f * g')%F a b Ifg' -> Rint (f' * g)%F a b If'g -> Ifg' = f b * g b - f a * g a - If'g.
proof: Proof. intros f g a b f' g' Ifg' If'g Hab Hderf Hderg Hcontf' Hcontg' Hfg' Hf'g. assert (H : forall a b c, a + b = c -> a = c - b) by (intros; subst; ring); apply H; clear H. apply Rint_uniqueness with (f * g' + f' * g)%F a b. apply Rint_plus; assumption. replace (f b * g b - f a * g a) with ((f * g)%F b - (f * g)%F a) by reflexivity. apply Rint_derive. assumption. intros; unfold mult_fct, plus_fct; rewrite Rplus_comm; apply derivable_pt_lim_mult; intuition. intros; apply continuity_pt_plus; apply continuity_pt_mult; try intuition; apply derivable_continuous_pt. exists (f' x); apply Hderf; intuition. exists (g' x); apply Hderg; intuition. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions