# Library Coqtail.mytheories.myReals.MyRfunctions

Require Import Reals.
Require Import Fourier.
Require Export Rfunctions.

Open Scope R_scope.

Power

Lemma Rpow_mult_distr : x y n, (x × y) ^ n = x ^ n × y ^ n.
Proof.
intros x y n; induction n; simpl.
field.
repeat (rewrite Rmult_assoc); apply Rmult_eq_compat_l.
rewrite IHn; field.
Qed.

Distance

Lemma R_dist_ge_l : x y z, R_dist x y zRabs x Rabs y + z.
Proof.
unfold R_dist; unfold Rabs.
intros x y z H.
repeat destruct Rcase_abs; fourier.
Qed.

Lemma R_dist_gt_l : x y z, R_dist x y < zRabs x < Rabs y + z.
Proof.
unfold R_dist; unfold Rabs.
intros x y z H.
repeat destruct Rcase_abs; fourier.
Qed.

Lemma R_dist_ge_r : x y z, R_dist x y zRabs y - z Rabs x.
Proof.
unfold R_dist; unfold Rabs.
intros x y z H.
repeat destruct Rcase_abs; fourier.
Qed.

Lemma R_dist_gt_r : x y z, R_dist x y < zRabs y - z < Rabs x.
Proof.
unfold R_dist; unfold Rabs.
intros x y z H.
repeat destruct Rcase_abs; fourier.
Qed.

Lemma continuity_pt_constant : c x, continuity_pt (fct_cte c) x.
Proof.
intros c x ; apply continuity_const.
intros u y; reflexivity.
Qed.

Lemma continuity_constant : c, continuity (fct_cte c).
Proof.
intro c; apply continuity_const.
intros x y; reflexivity.
Qed.

C1 continuation of a C1 function on a segment

Section Rint_C1.

Definition C1_continuation f a b d:=
fun x : R
if Rlt_dec x a then d a × (x - a) + f a
else if Rle_dec x b then f x else d b × (x - b) + f b .

Definition C1_continuation_derive d a b : RR :=
fun x : R
if Rlt_dec x a then d a
else if Rle_dec x b then d x else d b.

Lemma C1_continuation_eq : f a b d x,
a x bC1_continuation f a b d x = f x.
Proof.
intros f a b d x Hx.
unfold C1_continuation.
destruct (Rlt_dec x a).
apply False_ind; apply (Rlt_not_le _ _ r), (proj1 Hx).

destruct (Rle_dec x b).
reflexivity.

apply False_ind, n0, (proj2 Hx).
Qed.

Lemma C1_continuation_derive_eq : a b d x,
a x bC1_continuation_derive d a b x = d x.
Proof.
intros a b d x Hx.
unfold C1_continuation_derive.
destruct (Rlt_dec x a).
apply False_ind; apply (Rlt_not_le _ _ r), (proj1 Hx).

destruct (Rle_dec x b).
reflexivity.

apply False_ind, n0, (proj2 Hx).
Qed.

Lemma prolongement_C1_derivable : (f d : RR) (a b : R),
a b
( c, a c bderivable_pt_abs f c (d c)) →
{ derg | x, derive (C1_continuation f a b d) derg x =
C1_continuation_derive d a b x}.
Proof.
intros f d a b Hab Hder.
assert (Hrew : c u v, v 0 → (c × (u + v - u) + f u - f u) / v - d u = c - d u)
by ( intros; field; assumption).

assert (Hrew2 : u x h z, h 0 → ((u × (x + h - z) + f z -(u × (x - z) + f z)) / h - u) = 0) by
(intros; field; assumption).
assert( x, derivable_pt_abs (C1_continuation f a b d) x (C1_continuation_derive d a b x)).
intro x.
unfold C1_continuation, C1_continuation_derive, derivable_pt_abs, derivable_pt_lim.
destruct (Rlt_dec x a) as [Hxa | Hax].
destruct (Rle_dec x b) as [Hxb | Hxb].
intros eps Heps.
(mkposreal (a-x) (Rgt_minus _ _ Hxa)).
intros h hneq Hcond.
destruct(Rlt_dec (x+h) a) as [Hxha | Hxha].
rewrite Hrew2, Rabs_R0; assumption; apply Heps.

apply False_ind, Hxha.
apply Rle_lt_trans with (x+ Rabs h).
apply Rplus_le_compat_l.
apply RRle_abs.
replace a with (x + a + -x) by ring.
rewrite Rplus_assoc; apply Rplus_lt_compat_l.
apply Hcond.

apply False_ind, Hxb.
apply Rle_trans with a; intuition.
destruct (Rle_dec x b) as [Hxb | Hxb].
intros eps Heps.
apply Rnot_lt_le in Hax.
assert (Hx : a x b) by (split;assumption).
destruct (Hder x Hx eps Heps) as [delta Hdelta].
destruct Hxb as [Hxb | Hxb].
destruct Hax as [Hax |Hax].         assert (0 < Rmin delta (Rmin (b-x) (x - a))) as Hposreal.
apply Rmin_pos.
apply cond_pos.
apply Rmin_pos; fourier.
(mkposreal _ Hposreal).
intros h hneq Hcond.
destruct(Rlt_dec (x+h) a) as [Hxha | Hxha].
apply False_ind; apply (Rlt_not_le _ _ Hxha).
assert(- h < x - a) as Hf.
apply Rle_lt_trans with (Rabs h).
rewrite <- Rabs_Ropp; apply RRle_abs.

apply Rlt_le_trans with (Rmin (b - x) (x - a)).
apply (proj2 ((Rmin_Rgt_l delta (Rmin (b - x) (x - a)) (Rabs h) Hcond))).
apply Rmin_r.
fourier.
destruct (Rle_dec (x+h) b) as [Hxhb | Hxhb].
apply (Hdelta _ hneq).
apply (proj1 (Rmin_Rgt_l delta _ _ Hcond)).

apply False_ind, Hxhb.
replace b with (x + (b - x)) by ring.
apply Rplus_le_compat_l.
apply Rle_trans with (Rabs h).
apply RRle_abs.
apply Rle_trans with (Rmin (b - x) (x - a)).
left; apply (proj2 ((Rmin_Rgt_l delta _ (Rabs h) Hcond))).
apply Rmin_l.

subst x.         assert( Hposreal : 0 < Rmin delta (b-a)).
apply Rmin_pos.
apply cond_pos.
fourier.
(mkposreal _ Hposreal).
intros h hneq Hcond.
destruct (Rlt_dec (a + h) a) as [Hah | Hah].
rewrite Hrew.
ring_simplify (d a - d a).
rewrite Rabs_R0; apply Heps.
apply hneq.
destruct(Rle_dec (a+h) b) as [Hh | Hh].
apply (Hdelta h hneq).
apply Rlt_le_trans with (Rmin delta (b-a)).
apply Hcond.
apply Rmin_l.
apply False_ind, Hh.
replace b with (a + (b-a)) by ring.
apply Rplus_le_compat_l.
apply Rle_trans with (Rabs h).
apply RRle_abs.
apply Rle_trans with (Rmin delta (b-a)).
left; apply Hcond.
apply Rmin_r.

subst x.         destruct Hax as [Hax | Hax].
assert( Hposreal : 0 < Rmin delta (b-a)).
apply Rmin_pos.
apply cond_pos.
fourier.
(mkposreal _ Hposreal).
intros h hneq Hcond.
destruct (Rlt_dec (b + h) a) as [Hbh | Hbh].
apply False_ind, (Rlt_not_le _ _ Hbh).
assert(- h b - a) as Hf.
apply Rle_trans with (Rabs h).
rewrite <- Rabs_Ropp; apply RRle_abs.
apply Rle_trans with (Rmin delta (b - a)).
intuition.
apply Rmin_r.
fourier.

destruct(Rle_dec (b+h) b) as [Hh | Hh].
apply (Hdelta h hneq).
apply Rlt_le_trans with (Rmin delta (b - a)).
apply Hcond.
apply Rmin_l.
rewrite Hrew.
ring_simplify ( d b - d b).
rewrite Rabs_R0; apply Heps.
apply hneq.

subst b.              delta.
intros h hneq Hcond.
destruct(Rlt_dec (a+h) a).

rewrite Hrew.
ring_simplify ( d a - d a).
rewrite Rabs_R0; apply Heps.
apply hneq.

destruct (Rle_dec (a+h) a) as [Hh | Hh].
intuition.
rewrite Hrew.
ring_simplify ( d a - d a).
rewrite Rabs_R0; apply Heps.
apply hneq.

destruct (Rle_dec x b).
intros eps Heps.
apply Rnot_le_lt in Hxb.
(mkposreal (x - b) (Rgt_minus _ _ Hxb)).
intros h hneq Hcond.
destruct(Rlt_dec (x+h) a) as [Hxha | Hxha].
apply False_ind, (RIneq.Rle_not_lt _ _ Hab).
apply Rlt_le_trans with (x+h).
assert(- h x - b) as Hf.
apply Rle_trans with (Rabs h).
rewrite <- Rabs_Ropp; apply RRle_abs.
intuition.
fourier.
intuition.

destruct (Rle_dec (x + h) b) as [Hh | Hh].
apply False_ind, (RIneq.Rle_not_lt _ _ Hh).
assert(- h x - b) as Hf.
apply Rle_trans with (Rabs h).
rewrite <- Rabs_Ropp; apply RRle_abs.
intuition.
fourier.

rewrite Hrew2, Rabs_R0; assumption; apply Heps.
intros eps Heps.

apply Rnot_le_lt in Hxb.
(mkposreal (x - b) (Rgt_minus _ _ Hxb)).
intros h hneq Hcond.
destruct(Rlt_dec (x+h) a) as [Hxha | Hxha].
apply False_ind, (RIneq.Rle_not_lt _ _ Hab).
apply Rlt_le_trans with (x+h).
assert(- h x - b) as Hf.
apply Rle_trans with (Rabs h).
rewrite <- Rabs_Ropp; apply RRle_abs.
intuition.
fourier.
intuition.

destruct (Rle_dec (x + h) b) as [Hh | Hh].
apply False_ind, (RIneq.Rle_not_lt _ _ Hh).
assert(- h < x - b) as Hf.
apply Rle_lt_trans with (Rabs h).
rewrite <- Rabs_Ropp; apply RRle_abs.
intuition.
fourier.

rewrite Hrew2, Rabs_R0; assumption.
assert(derivable (C1_continuation f a b d)) as der_c by
(intro x; (C1_continuation_derive d a b x); apply H).
der_c.
intro x.
unfold derive.
apply uniqueness_limite with (C1_continuation f a b d) x.
eapply derive_pt_eq_1.
reflexivity.

apply H.
Qed.

Lemma C0_sticking_one_pt : f gl gr a,
continuity glcontinuity gr
( x, x af x = gl x) →
( x, a xf x = gr x) →
continuity f.
Proof.
intros f gl gr a Hl Hr Hfl Hfr x.
destruct (Rtotal_order x a).

intros eps Heps.
destruct (Hl x eps); try assumption.
destruct H0.
destruct (Rlt_dec x0 (a - x)).
x0; split; try assumption.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) Rabs (x1 - x)) by apply RRle_abs.
fourier.
repeat rewrite Hfl.
apply (H1 x1). fourier.
apply Rnot_lt_le; assumption.

apply Rnot_lt_le in n.
(a - x); split; try fourier.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) Rabs (x1 - x)) by apply RRle_abs.
fourier.
assert (D_x no_cond x x1 dist R_met x1 x < x0
dist R_met (gl x1) (gl x) < eps) by (exact (H1 x1)).
apply Rnot_lt_le in n0.
repeat rewrite Hfl; try fourier.
intros; destruct H3.
apply H2.
split; try assumption.
fourier.

destruct H.
intros eps Heps.
rewrite H in |-*; clear x H.
destruct (Hl a eps); try assumption.
destruct (Hr a eps); try assumption.
destruct H; destruct H0.
(Rmin x x0); split.
apply Rmin_pos; assumption.
intro x1; destruct (Rlt_dec x1 a).
repeat rewrite Hfl; try fourier.
assert (D_x no_cond a x1 dist R_met x1 a < x
dist R_met (gl x1) (gl a) < eps) by (exact (H1 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x x0 x) by exact (Rmin_l x x0).
fourier.
apply Rnot_lt_le in n.
repeat rewrite Hfr; try fourier.
assert (D_x no_cond a x1 dist R_met x1 a < x0
dist R_met (gr x1) (gr a) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x x0 x0) by exact (Rmin_r x x0).
fourier.

intros eps Heps.
destruct (Hr x eps); try assumption.
destruct H0.
destruct (Rlt_dec x0 (x - a)).
x0; split; try assumption.
intro.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert (x - x1 Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
fourier.
repeat rewrite Hfr.
apply (H1 x1). fourier.
apply Rnot_lt_le; assumption.

(x - a); split; try fourier.
intro.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert (x - x1 Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
fourier.
apply Rnot_lt_le in n0.
repeat rewrite Hfr; try fourier.
apply Rnot_lt_le in n.
assert (D_x no_cond x x1 dist R_met x1 x < x0
dist R_met (gr x1) (gr x) < eps) by (exact (H1 x1)).
intros; destruct H3.
apply H2.
split; try assumption.
fourier.
Qed.

Lemma C0_sticking_one_pt_strong : f gl gr a,
( x, x acontinuity_pt gl x) →
( x, a xcontinuity_pt gr x) →
( x, x af x = gl x) →
( x, a xf x = gr x) →
continuity f.
Proof.
intros f gl gr a Hl Hr Hfl Hfr x.
destruct (Rtotal_order x a) as [|[]].
intros eps Heps.
destruct (Hl x (Rlt_le _ _ H) eps); try assumption.
destruct H0.
destruct (Rlt_dec x0 (a - x)).
x0; split; try assumption.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) Rabs (x1 - x)) by apply RRle_abs.
fourier.
repeat rewrite Hfl.
apply (H1 x1). fourier.
apply Rnot_lt_le; assumption.

apply Rnot_lt_le in n.
(a - x); split; try fourier.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) Rabs (x1 - x)) by apply RRle_abs.
fourier.
assert (D_x no_cond x x1 dist R_met x1 x < x0
dist R_met (gl x1) (gl x) < eps) by (exact (H1 x1)).
apply Rnot_lt_le in n0.
repeat rewrite Hfl; try fourier.
intros; destruct H3.
apply H2.
split; try assumption.
fourier.

intros eps Heps.
rewrite H in |-*; clear H x.
destruct (Hl a (Rle_refl a) eps); try assumption.
destruct (Hr a (Rle_refl a) eps); try assumption.
destruct H; destruct H0.
(Rmin x x0); split.
apply Rmin_pos; assumption.
intro x1; destruct (Rlt_dec x1 a).
repeat rewrite Hfl; try fourier.
assert (D_x no_cond a x1 dist R_met x1 a < x
dist R_met (gl x1) (gl a) < eps) by (exact (H1 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x x0 x) by exact (Rmin_l x x0).
fourier.
apply Rnot_lt_le in n.
repeat rewrite Hfr; try fourier.
assert (D_x no_cond a x1 dist R_met x1 a < x0
dist R_met (gr x1) (gr a) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x x0 x0) by exact (Rmin_r x x0).
fourier.

intros eps Heps.
destruct (Hr x (Rlt_le _ _ H) eps); try assumption.
destruct H0.
destruct (Rlt_dec x0 (x - a)).
x0; split; try assumption.
intro.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert (x - x1 Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
fourier.
repeat rewrite Hfr.
apply (H1 x1). fourier.
apply Rnot_lt_le; assumption.

(x - a); split; try fourier.
intro.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert (x - x1 Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
fourier.
apply Rnot_lt_le in n0.
repeat rewrite Hfr; try fourier.
apply Rnot_lt_le in n.
assert (D_x no_cond x x1 dist R_met x1 x < x0
dist R_met (gr x1) (gr x) < eps) by (exact (H1 x1)).
intros; destruct H3.
apply H2.
split; auto.
fourier.
Qed.

Lemma C0_sticking_two_pt : f gl gc gr a b,
a b
continuity gl
( x, a x bcontinuity_pt gc x) →
continuity gr
( x, x af x = gl x) →
( x, a x bf x = gc x) →
( x, b xf x = gr x) →
continuity f.
Proof.
intros f gl gc gr a b Hab Hl Hc Hr Hfl Hfc Hfr x.
destruct ((Rle_lt_or_eq_dec a b) Hab).
destruct (Rtotal_order x a).

intros eps Heps.
destruct (Hl x eps); try assumption.
destruct H0.
(Rmin x0 (a-x)); split.
repeat (apply Rmin_pos); fourier.
intro.
destruct (Rlt_dec a x1).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H2; simpl in H3; unfold R_dist in H3.
assert ((x1 - x) Rabs (x1 - x)) by apply RRle_abs.
assert (Rmin x0 (a - x) a - x) by exact (Rmin_r x0 (a - x)).
fourier.
apply Rnot_lt_le in n.
repeat rewrite Hfl; try fourier.
assert (D_x no_cond x x1 dist R_met x1 x < x0
dist R_met (gl x1) (gl x) < eps) by (exact (H1 x1)).
intros; destruct H3.
apply H2.
split; try assumption.
assert (Rmin x0 (a - x) x0) by exact (Rmin_l x0 (a - x)).
fourier.

destruct H.
rewrite H in |-*; clear x H.
intros eps Heps.
destruct (Hl a eps); try assumption.
destruct (Hc a (conj (Rle_refl a) (Rlt_le _ _ r)) eps); try assumption.
destruct H; destruct H0.
(Rmin x (Rmin x0 (b-a))); split.
repeat (apply Rmin_pos); fourier.
intro x1; destruct (Rlt_dec x1 a).
repeat rewrite Hfl; try fourier.
assert (D_x no_cond a x1 dist R_met x1 a < x
dist R_met (gl x1) (gl a) < eps) by (exact (H1 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x (Rmin x0 (b-a)) x) by exact (Rmin_l x (Rmin x0 (b-a))).
fourier.

apply Rnot_lt_le in n.
destruct (Rlt_dec b x1).
intros.
assert False; try contradiction.
apply (Rgt_asym b x1); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert ((x1 - a) Rabs (x1 - a)) by apply RRle_abs.
assert (Rmin x (Rmin x0 (b-a)) (b-a)).
assert (Rmin x (Rmin x0 (b-a)) (Rmin x0 (b-a)))
by exact (Rmin_r x (Rmin x0 (b-a))).
assert ((Rmin x0 (b-a)) (b-a)) by exact (Rmin_r x0 (b-a)).
fourier.
fourier.
apply Rnot_lt_le in n0.
repeat rewrite Hfc; try split; try fourier.
assert (D_x no_cond a x1 dist R_met x1 a < x0
dist R_met (gc x1) (gc a) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x (Rmin x0 (b-a)) x0).
assert (Rmin x (Rmin x0 (b-a)) (Rmin x0 (b-a)))
by exact (Rmin_r x (Rmin x0 (b-a))).
assert ((Rmin x0 (b-a)) x0) by exact (Rmin_l x0 (b-a)).
fourier.
fourier.

destruct (Rtotal_order x b).
intros eps Heps.
destruct (Hc x (conj (Rlt_le _ _ H) (Rlt_le _ _ H0)) eps); try assumption.
destruct H1.
(Rmin (Rmin (x-a) (b-x)) x0); split.
repeat (apply Rmin_pos); fourier.
intro x1.
destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym a x1); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert (x - x1 Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
assert ((Rmin (Rmin (x-a) (b-x)) x0) (x-a)).
assert ((Rmin (Rmin (x-a) (b-x)) x0) (Rmin (x-a) (b-x)))
by exact (Rmin_l (Rmin (x-a) (b-x)) x0).
assert ((Rmin (x-a) (b-x)) x-a) by exact (Rmin_l (x-a) (b-x)).
fourier.
fourier.
destruct (Rlt_dec b x1).
intros.
assert False; try contradiction.
apply (Rgt_asym x1 b); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert (x1 - x Rabs (x1 - x)) by apply RRle_abs.
assert ((Rmin (Rmin (x-a) (b-x)) x0) (b-x)).
assert ((Rmin (Rmin (x-a) (b-x)) x0) (Rmin (x-a) (b-x)))
by exact (Rmin_l (Rmin (x-a) (b-x)) x0).
assert ((Rmin (x-a) (b-x)) b-x) by exact (Rmin_r (x-a) (b-x)).
fourier.
fourier.
apply Rnot_lt_le in n.
apply Rnot_lt_le in n0.
assert (D_x no_cond x x1 dist R_met x1 x < x0
dist R_met (gc x1) (gc x) < eps) by (exact (H2 x1)).
repeat rewrite Hfc; try split; try fourier.
intros; destruct H4.
apply H3.
split; try assumption.
assert ((Rmin (Rmin (x-a) (b-x)) x0) x0)
by exact (Rmin_r (Rmin (x-a) (b-x)) x0).
fourier.

destruct H0.
rewrite H0 in |-*; clear H x H0.
intros eps Heps.
destruct (Hc b (conj (Rlt_le _ _ r) (Rle_refl b)) eps); try assumption.
destruct (Hr b eps); try assumption.
destruct H; destruct H0.
(Rmin x (Rmin x0 (b-a))); split.
repeat (apply Rmin_pos); fourier.
intro x1; destruct (Rlt_dec b x1).
repeat rewrite Hfr; try fourier.
assert (D_x no_cond b x1 dist R_met x1 b < x0
dist R_met (gr x1) (gr b) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x (Rmin x0 (b-a)) x0).
assert (Rmin x (Rmin x0 (b-a)) (Rmin x0 (b-a)))
by exact (Rmin_r x (Rmin x0 (b-a))).
assert ((Rmin x0 (b-a)) x0) by exact (Rmin_l x0 (b-a)).
fourier.
fourier.

destruct (Rlt_dec x1 a).
intros.
assert False; try contradiction.
apply (Rgt_asym x1 a); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert ((b - x1) Rabs (x1 - b)).
rewrite Rabs_minus_sym; apply RRle_abs.
assert (Rmin x (Rmin x0 (b-a)) (b-a)).
assert (Rmin x (Rmin x0 (b-a)) (Rmin x0 (b-a)))
by exact (Rmin_r x (Rmin x0 (b-a))).
assert ((Rmin x0 (b-a)) (b-a)) by exact (Rmin_r x0 (b-a)).
fourier.
fourier.
apply Rnot_lt_le in n.
apply Rnot_lt_le in n0.
repeat rewrite Hfc; try split; try fourier.
assert (D_x no_cond b x1 dist R_met x1 b < x
dist R_met (gc x1) (gc b) < eps) by (exact (H1 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x (Rmin x0 (b-a)) x) by exact (Rmin_l x (Rmin x0 (b-a))).
fourier.

intros eps Heps.
destruct (Hr x eps); try assumption.
destruct H1.
(Rmin x0 (x - b)); split.
repeat (apply Rmin_pos); fourier.
intro.
destruct (Rlt_dec x1 b).
intros.
assert False; try contradiction.
apply (Rgt_asym b x1); try assumption.
destruct H3; simpl in H4; unfold R_dist in H4.
assert ((x - x1) Rabs (x1 - x)).
rewrite Rabs_minus_sym; apply RRle_abs.
assert (Rmin x0 (x - b) x - b) by exact (Rmin_r x0 (x - b)).
fourier.
apply Rnot_lt_le in n.
repeat rewrite Hfr; try fourier.
assert (D_x no_cond x x1 dist R_met x1 x < x0
dist R_met (gr x1) (gr x) < eps) by (exact (H2 x1)).
intros; destruct H4.
apply H3.
split; try assumption.
assert (Rmin x0 (x - b) x0) by exact (Rmin_l x0 (x - b)).
fourier.

rewrite e in *|-.
apply (C0_sticking_one_pt f gl gr b); assumption.
Qed.

Lemma C1_continuation_derive_continuous : d a b, a b
( c, a c bcontinuity_pt d c) →
continuity (C1_continuation_derive d a b).
Proof.
intros d a b Hab Cd.
apply (C0_sticking_two_pt _ (fct_cte (d a)) d (fct_cte (d b)) a b Hab);
try (apply continuity_constant); auto; intros;
unfold C1_continuation_derive;
destruct (Rlt_dec x a);
destruct (Rle_dec x b); auto.

assert (x = a) by (apply Rle_antisym; auto; apply Rnot_lt_le; auto).
subst; trivial.

pose proof Rle_antisym a x (Rnot_lt_le _ _ n) H; subst.
apply (False_ind _ (n0 Hab)).

apply (False_ind _ (RIneq.Rle_not_lt _ _ (proj1 H) r)).

apply (False_ind _ (RIneq.Rle_not_lt _ _ (proj1 H) r)).

apply (False_ind _ (n0 (proj2 H))).

assert (x = b) by (apply Rle_antisym; auto; apply Rnot_lt_le; auto); subst.
apply (False_ind _ (RIneq.Rle_not_lt _ _ Hab r)).

apply False_ind; apply (RIneq.Rle_not_lt _ _ H).
apply Rlt_le_trans with a; auto.

assert (x = b) by (apply Rle_antisym; auto; apply Rnot_lt_le; auto); subst.
trivial.
Qed.

Lemma prolongement_C1_C1 : (f d : RR) (a b : R),
a b
( c, a c bderivable_pt_abs f c (d c)) →
( c, a c bcontinuity_pt d c) →
{g : C1_fun |
( c : R, a c bf c = g c)
( c : R, a c bd c = derive g (diff0 g) c)}.
Proof.
intros f d a b Hab Hder Hcont.
pose proof (prolongement_C1_derivable f d a b Hab Hder) as [diff0 Heq].
pose proof (C1_continuation_derive_continuous d a b Hab Hcont) as cont.
assert(c1 : continuity (derive (C1_continuation f a b d) diff0)).
intros x eps Heps.
destruct (cont x eps Heps) as [alpha [Halpha1 Halpha2]].
alpha.
split.
assumption.
intros.
do 2 rewrite Heq; intuition.
(mkC1 c1).
split.
intros x Hx.
rewrite <- (C1_continuation_eq f a b d x Hx);
reflexivity.

intros x Hx.
rewrite <- (C1_continuation_derive_eq a b d x Hx), Heq;
reflexivity.
Qed.

End Rint_C1.

Create HintDb Rcont.

Hint Resolve continuity_pt_plus : Rcont.
Hint Resolve continuity_pt_mult : Rcont.
Hint Resolve continuity_pt_minus : Rcont.
Hint Resolve continuity_pt_opp : Rcont.
Hint Resolve continuity_pt_const : Rcont.
Hint Resolve continuity_pt_inv : Rcont.
Hint Resolve continuity_pt_div : Rcont.
Hint Resolve continuity_pt_comp : Rcont.
Hint Resolve continuity_pt_sqrt : Rcont.
Hint Resolve continuity_pt_constant : Rcont.
Hint Resolve derivable_continuous_pt : Rcont.

Hint Resolve continuity_plus : Rcont.
Hint Resolve continuity_mult : Rcont.
Hint Resolve continuity_minus : Rcont.
Hint Resolve continuity_opp : Rcont.
Hint Resolve continuity_const : Rcont.
Hint Resolve continuity_inv : Rcont.
Hint Resolve continuity_div : Rcont.
Hint Resolve continuity_constant : Rcont.
Hint Resolve continuity_comp : Rcont.
Hint Resolve derivable_continuous : Rcont.

Hint Resolve derivable_pt_plus : Rcont.
Hint Resolve derivable_pt_mult : Rcont.
Hint Resolve derivable_pt_minus: Rcont.
Hint Resolve derivable_pt_opp : Rcont.
Hint Resolve derivable_pt_const : Rcont.
Hint Resolve derivable_pt_inv : Rcont.
Hint Resolve derivable_pt_div : Rcont.
Hint Resolve derivable_pt_comp : Rcont.
Hint Resolve derivable_pt_sqrt : Rcont.
Hint Resolve derivable_pt_exp : Rcont.
Hint Resolve derivable_pt_id : Rcont.
Hint Resolve derivable_pt_pow : Rcont.
Hint Resolve derivable_pt_cosh : Rcont.

Hint Resolve derivable_plus : Rcont.
Hint Resolve derivable_mult : Rcont.
Hint Resolve derivable_minus : Rcont.
Hint Resolve derivable_opp : Rcont.
Hint Resolve derivable_const : Rcont.
Hint Resolve derivable_inv : Rcont.
Hint Resolve derivable_div : Rcont.
Hint Resolve derivable_comp : Rcont.
Hint Resolve derivable_continuous : Rcont.
Hint Resolve derivable_cos : Rcont.
Hint Resolve derivable_sin : Rcont.
Hint Resolve derivable_exp : Rcont.
Hint Resolve derivable_id : Rcont.
Hint Resolve derivable_id : Rcont.
Hint Resolve derivable_pow : Rcont.
Hint Resolve derivable_cosh : Rcont.

Hint Resolve derivable_pt_lim_sin : Rcont.
Hint Resolve derivable_pt_lim_cos : Rcont.
Hint Resolve derivable_pt_lim_sqrt : Rcont.
Hint Resolve derivable_pt_lim_ln : Rcont.
Hint Resolve derivable_pt_lim_exp : Rcont.
Hint Resolve derivable_pt_lim_plus: Rcont.
Hint Resolve derivable_pt_lim_mult: Rcont.
Hint Resolve derivable_pt_lim_minus : Rcont.
Hint Resolve derivable_pt_lim_opp : Rcont.
Hint Resolve derivable_pt_lim_const : Rcont.
Hint Resolve derivable_pt_lim_id : Rcont.
Hint Resolve derivable_pt_lim_div : Rcont.
Hint Resolve derivable_pt_lim_comp : Rcont.
Hint Resolve derivable_pt_lim_pow : Rcont.
Hint Resolve derivable_pt_lim_power : Rcont.
Hint Resolve derivable_pt_lim_id : Rcont.
Hint Resolve derivable_pt_lim_cosh : Rcont.