proposition: Lemma derivable_pt_lim_minus : forall f1 f2 (x l1 l2:R), derivable_pt_lim f1 x l1 -> derivable_pt_lim f2 x l2 -> derivable_pt_lim (f1 - f2) x (l1 - l2).
proof: Proof. intros. apply uniqueness_step3. assert (H1 := uniqueness_step2 _ _ _ H). assert (H2 := uniqueness_step2 _ _ _ H0). unfold minus_fct. cut (forall h:R, (f1 (x + h) - f1 x) / h - (f2 (x + h) - f2 x) / h = (f1 (x + h) - f2 (x + h) - (f1 x - f2 x)) / h). - intro. generalize (limit_minus (fun h':R => (f1 (x + h') - f1 x) / h') (fun h':R => (f2 (x + h') - f2 x) / h') (fun h:R => h <> 0) l1 l2 0 H1 H2). unfold limit1_in; unfold limit_in; unfold dist; simpl; unfold Rdist; intros. elim (H4 eps H5); intros. exists x0. elim H6; intros. split. + assumption. + intros; rewrite <- H3; apply H8; assumption. - intro; unfold Rdiv; ring. Qed.
imports: Rbase Rfunctions Rlimit Rderiv