proposition: Lemma primitive_diff : forall f g fp : (R->R), (forall x:R, derivable_pt_lim f x (fp x))-> (forall x:R, derivable_pt_lim g x (fp x))-> forall x:R, f x=(plus_fct g (fct_cte ((f 0)-(g 0)))) x.
proof: Proof. intros f g fp fder gder. assert(forall x:R, derivable_pt_lim (f-g) x ((fun _ => 0) x)) as fmpder. intro x. rewrite<-(Rminus_diag_eq _ _ (eq_refl (fp x))). apply derivable_pt_lim_minus. apply fder. apply gder. intro x. unfold plus_fct,fct_cte. assert((f-g)%F x=(f-g)%F 0) as diffeq. destruct (total_order_T x 0) as [xneg|xin]; try destruct xneg as [xin|x0]; try (rewrite x0; reflexivity); pose proof (MVT_cor2 (f-g)%F (fun _ => 0) _ _ xin (fun x _ => fmpder x)) as mvt; destruct mvt as [c mvt]; destruct mvt as [mvt ineq]; rewrite Rmult_0_l in mvt; pose proof (Rminus_diag_uniq _ _ mvt) as eqfi; rewrite eqfi; reflexivity. unfold minus_fct in diffeq. rewrite<-diffeq. field. Qed.
imports: Reals