proposition: Lemma derive_pt_plus : forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x), derive_pt (f1 + f2) x (derivable_pt_plus _ _ _ pr1 pr2) = derive_pt f1 x pr1 + derive_pt f2 x pr2.
proof: Proof. intros. assert (H := derivable_derive f1 x pr1). assert (H0 := derivable_derive f2 x pr2). assert (H1 := derivable_derive (f1 + f2)%F x (derivable_pt_plus _ _ _ pr1 pr2)). elim H; clear H; intros l1 H. elim H0; clear H0; intros l2 H0. elim H1; clear H1; intros l H1. rewrite H; rewrite H0; apply derive_pt_eq_0. assert (H3 := proj2_sig pr1). unfold derive_pt in H; rewrite H in H3. assert (H4 := proj2_sig pr2). unfold derive_pt in H0; rewrite H0 in H4. apply derivable_pt_lim_plus; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv