proposition: Lemma differentiable_pt_lim_minus : forall f1 f2 x v l1 l2, v <> C0 -> differentiable_pt_lim f1 x v l1 -> differentiable_pt_lim f2 x v l2 -> differentiable_pt_lim (f1 - f2) x v (l1 - l2).
proof: Proof. intros f1 f2 x v l1 l2 v_neq H H0. apply uniqueness_step3. assert (H1 := uniqueness_step2 _ _ _ _ v_neq H). assert (H2 := uniqueness_step2 _ _ _ _ v_neq H0). unfold minus_fct in |- *. cut (forall h, (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' => (f1 (x + h') - f1 x) / h') (fun h' => (f2 (x + h') - f2 x) / h') (fun u => u <> 0 /\ (exists h : R, h * u = v)) l1 l2 0 H1 H2). unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *; simpl in |- *; unfold R_dist in |- *; intros. elim (H4 eps H5); intros. exists x0. elim H6; intros. split. assumption. intros; rewrite <- H3; apply H8; assumption. intro; unfold Cdiv in |- *; ring. Qed.
imports: Cprop_base Cnorm Ctacfield Canalysis_def