proposition: Lemma primitive_eq: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))-> f 0=g 0-> forall x:R, f x=g x.
proof: Proof. intros f g fp fder gder init x. transitivity ((plus_fct g (fct_cte ((f 0)-(g 0)))) x). rewrite (primitive_diff f g fp); try assumption; try reflexivity. unfold plus_fct,fct_cte. rewrite init. field. Qed.
imports: Reals