proposition: Lemma antiderivative_Ucte : forall (f g1 g2:R -> R) (a b:R), antiderivative f g1 a b -> antiderivative f g2 a b -> exists c : R, (forall x:R, a <= x <= b -> g1 x = g2 x + c).
proof: Proof. unfold antiderivative; intros; elim H; clear H; intros; elim H0; clear H0; intros H0 _; exists (g1 a - g2 a); intros; assert (H3 : forall x:R, a <= x <= b -> derivable_pt g1 x). { intros; unfold derivable_pt; exists (f x0); elim (H x0 H3); intros; eapply derive_pt_eq_1; symmetry ; apply H4. } assert (H4 : forall x:R, a <= x <= b -> derivable_pt g2 x). { intros; unfold derivable_pt; exists (f x0); elim (H0 x0 H4); intros; eapply derive_pt_eq_1; symmetry ; apply H5. } assert (H5 : forall x:R, a < x < b -> derivable_pt (g1 - g2) x). { intros; elim H5; intros; apply derivable_pt_minus; [ apply H3; split; left; assumption | apply H4; split; left; assumption ]. } assert (H6 : forall x:R, a <= x <= b -> continuity_pt (g1 - g2) x). { intros; apply derivable_continuous_pt; apply derivable_pt_minus; [ apply H3 | apply H4 ]; assumption. } assert (H7 : forall (x:R) (P:a < x < b), derive_pt (g1 - g2) x (H5 x P) = 0). { intros; elim P; intros; apply derive_pt_eq_0; replace 0 with (f x0 - f x0); [ idtac | ring ]. assert (H9 : a <= x0 <= b). { split; left; assumption. } apply derivable_pt_lim_minus; [ elim (H _ H9) | elim (H0 _ H9) ]; intros; eapply derive_pt_eq_1; symmetry ; apply H10. } assert (H8 := null_derivative_loc (g1 - g2)%F a b H5 H6 H7); unfold constant_D_eq in H8; assert (H9 := H8 _ H2); unfold minus_fct in H9; rewrite <- H9; ring. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra