proposition: Lemma antiderivative_P1 : forall (f g F G:R -> R) (l a b:R), antiderivative f F a b -> antiderivative g G a b -> antiderivative (fun x:R => l * f x + g x) (fun x:R => l * F x + G x) a b.
proof: Proof. unfold antiderivative; intros; elim H; elim H0; clear H H0; intros; split. { intros; elim (H _ H3); elim (H1 _ H3); intros. assert (H6 : derivable_pt (fun x:R => l * F x + G x) x). { reg. } exists H6; symmetry ; reg; rewrite <- H4; rewrite <- H5; ring. } assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis