proposition: Lemma antiderivative_P4 : forall (f F0 F1:R -> R) (a b c:R), antiderivative f F0 a b -> antiderivative f F1 a c -> antiderivative f F1 b c \/ antiderivative f F0 c b.
proof: Proof. intros; unfold antiderivative in H, H0; elim H; clear H; elim H0; clear H0; intros; destruct (total_order_T c b) as [[Hlt|Heq]|Hgt]. - right; unfold antiderivative; split. { intros; apply H1; elim H3; intros; split; [ apply Rle_trans with c; assumption | assumption ]. } left; assumption. - right; unfold antiderivative; split. { intros; apply H1; elim H3; intros; split; [ apply Rle_trans with c; assumption | assumption ]. } right; assumption. - left; unfold antiderivative; split. { intros; apply H; elim H3; intros; split; [ apply Rle_trans with b; assumption | assumption ]. } left; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis