(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Section ycngftys.

Require Import Reals.
Require Import trajectory_const.
Require Import rrho.
Require Import trajectory_def.
Require Import constants.

Unset Standard Proposition Elimination Names.

Variable intr : Trajectory.

(**********)
Definition xi : R -> R := x intr.
Definition yi : R -> R := y intr.
Definition vi : TypeSpeed := h intr.
Definition xP (t : R) : R := (xi t - xi 0)%R.
Definition yP (t : R) : R := (yi t - yi 0)%R.
Definition u (eps : posreal) (t : R) : R :=
  sqrt (Rsqr (xP t) + Rsqr (yP t) + Rsqr eps).
Definition u0 (t : R) : R := sqrt (Rsqr (xP t) + Rsqr (yP t)).

(**********)
Lemma xi_derivable : derivable xi.
(* Goal: derivable xi *)
unfold xi in |- *; apply (cond_diff (x intr)).
Qed.

Lemma yi_derivable : derivable yi.
(* Goal: derivable yi *)
unfold yi in |- *; apply (cond_diff (y intr)).
Qed.

Lemma xP_derivable : derivable xP.
(* Goal: derivable xP *)
unfold xP in |- *.
(* Goal: derivable (fun t : R => Rminus (xi t) (xi (IZR Z0))) *)
reg; apply xi_derivable.
Qed.

Lemma yP_derivable : derivable yP.
(* Goal: derivable yP *)
unfold yP in |- *.
(* Goal: derivable (fun t : R => Rminus (yi t) (yi (IZR Z0))) *)
reg; apply yi_derivable.
Qed.

(**********)
Lemma d_u : forall eps : posreal, derivable (fun t : R => u eps t).
(* Goal: forall eps : posreal, derivable (fun t : R => u eps t) *)
intro.
(* Goal: forall eps : posreal, derivable (fun t : R => u eps t) *)
unfold u in |- *; unfold derivable in |- *; intro.
(* Goal: derivable (fun t : R => Rmult (v vi) t) *)
reg.
(* Goal: derivable_pt yP t *)
(* Goal: derivable_pt xP t *)
apply yP_derivable.
(* Goal: derivable_pt xP t *)
apply xP_derivable.
(* Goal: Rlt (IZR Z0) (Rplus (Rplus (Rsqr (xP x)) (Rsqr (yP x))) (Rsqr (pos eps))) *)
apply Rle_lt_trans with (Rsqr (xP x) + Rsqr (yP x))%R.
(* Goal: Rle (IZR Z0) (Rplus (Rsqr (xP x)) (Rsqr (yP x))) *)
(* Goal: Rlt (Rplus (Rsqr (xP x)) (Rsqr (yP x))) (Rplus (Rplus (Rsqr (xP x)) (Rsqr (yP x))) (Rsqr (pos eps))) *)
apply Rplus_le_le_0_compat; apply Rle_0_sqr.
(* Goal: Rlt (Rplus (Rsqr (xP x)) (Rsqr (yP x))) (Rplus (Rplus (Rsqr (xP x)) (Rsqr (yP x))) (Rsqr (pos eps))) *)
rewrite Rplus_assoc.
(* Goal: Rlt (Rplus (Rsqr (yP x)) (IZR Z0)) (Rplus (Rsqr (yP x)) (Rsqr (pos eps))) *)
apply Rplus_lt_compat_l.
(* Goal: Rlt (Rsqr (yP x)) (Rplus (Rsqr (yP x)) (Rsqr (pos eps))) *)
pattern (Rsqr (yP x)) at 1 in |- *; rewrite <- Rplus_0_r.
(* Goal: Rlt (Rplus (Rsqr (yP x)) (IZR Z0)) (Rplus (Rsqr (yP x)) (Rsqr (pos eps))) *)
apply Rplus_lt_compat_l.
(* Goal: Rlt (IZR Z0) (Rsqr (pos eps)) *)
apply Rsqr_pos_lt.
red in |- *; intro; assert (H0 := cond_pos eps); rewrite H in H0;
 elim (Rlt_irrefl _ H0).
Qed.

Lemma fct_der2 :
 forall (eps : posreal) (t : R), derivable_pt (fun y : R => Rsqr (u eps y)) t.
(* Goal: derivable (fun t : R => Rmult (v vi) t) *)
intros; set (f := u eps); reg.
(* Goal: derivable_pt f t *)
apply (d_u eps).
Qed.

(**********)
Lemma D_Rsqr_u_epsilon_1 :
 forall (eps : posreal) (t : R),
 derive_pt (fun y : R => Rsqr (u eps y)) t (fct_der2 eps t) =
 (2 * u eps t * derive_pt (u eps) t (d_u eps t))%R. 
(* Goal: forall (eps : posreal) (t : R), @eq R (derive_pt (fun y : R => Rsqr (u eps y)) t (fct_der2 eps t)) (Rmult (Rmult (IZR (Zpos (xO xH))) (u eps t)) (derive_pt (u eps) t (d_u eps t))) *)
intros; set (f := u eps).
(* Goal: @eq R (derive_pt (fun y : R => Rsqr (f y)) t (fct_der2 eps t)) (Rmult (Rmult (IZR (Zpos (xO xH))) (f t)) (derive_pt f t (d_u eps t))) *)
cut (derivable_pt f t); [ intro H | apply (d_u eps t) ].
(* Goal: @eq R (derive_pt (fun y : R => Rsqr (f y)) t (fct_der2 eps t)) (Rmult (Rmult (IZR (Zpos (xO xH))) (f t)) (derive_pt f t (d_u eps t))) *)
cut (derive_pt f t H = derive_pt f t (d_u eps t)); [ intro | apply pr_nu ].
(* Goal: derivable (fun t : R => Rmult (v vi) t) *)
reg.
Qed.

(**********)
Lemma xP_derive :
 forall t : R,
 derive_pt xP t (xP_derivable t) = derive_pt xi t (xi_derivable t).
(* Goal: derivable (fun t : R => Rmult (v vi) t) *)
intro; unfold xP in |- *; reg.
(* Goal: @eq R (derive_pt yi t H) (derive_pt yi t (yi_derivable t)) *)
(* Goal: derivable_pt yi t *)
apply pr_nu.
(* Goal: derivable_pt xi t *)
apply xi_derivable.
Qed.

Lemma yP_derive :
 forall t : R,
 derive_pt yP t (yP_derivable t) = derive_pt yi t (yi_derivable t).
(* Goal: derivable (fun t : R => Rmult (v vi) t) *)
intro; unfold yP in |- *; reg.
(* Goal: @eq R (derive_pt yi t H) (derive_pt yi t (yi_derivable t)) *)
(* Goal: derivable_pt yi t *)
apply pr_nu.
(* Goal: derivable_pt yi t *)
apply yi_derivable.
Qed.

Lemma fct_der3 :
 forall (eps : posreal) (t : R),
 derivable_pt (fun y : R => (Rsqr (xP y) + (Rsqr (yP y) + Rsqr eps))%R) t.
(* Goal: derivable (fun t : R => Rmult (v vi) t) *)
intros; reg.
(* Goal: derivable_pt yP t *)
(* Goal: derivable_pt xP t *)
apply yP_derivable.
(* Goal: derivable_pt xP t *)
apply xP_derivable.
Qed.

(**********)
Lemma D_Rsqr_u_epsilon_2 :
 forall (eps : posreal) (t : R),
 (derive_pt (fun y : R => Rsqr (u eps y)) t (fct_der2 eps t) <= 2 * u0 t * vi)%R.
(* Goal: forall (eps : posreal) (t : R), @eq R (derive_pt (fun y : R => Rsqr (u eps y)) t (fct_der2 eps t)) (Rmult (Rmult (IZR (Zpos (xO xH))) (u eps t)) (derive_pt (u eps) t (d_u eps t))) *)
intros; set (f := u eps).
replace (derive_pt (fun y : R => Rsqr (f y)) t (fct_der2 eps t)) with
 (derive_pt (fun y : R => (Rsqr (xP y) + (Rsqr (yP y) + Rsqr eps))%R) t
    (fct_der3 eps t)).
replace
 (derive_pt (fun y : R => (Rsqr (xP y) + (Rsqr (yP y) + Rsqr eps))%R) t
    (fct_der3 eps t)) with
 (2 * derive_pt xP t (xP_derivable t) * xP t +
  2 * derive_pt yP t (yP_derivable t) * yP t)%R.
rewrite (xP_derive t).
rewrite (yP_derive t).
assert (H0 := cond_x intr t).
assert (H1 := cond_y intr t).
cut
 (derive_pt (x intr) t (cond_diff (x intr) t) =
  derive_pt xi t (xi_derivable t)); [ intro | apply pr_nu ].
cut
 (derive_pt (y intr) t (cond_diff (y intr) t) =
  derive_pt yi t (yi_derivable t)); [ intro | apply pr_nu ].
rewrite <- H; rewrite <- H2; rewrite H1; rewrite H0.
unfold vi in |- *.
repeat rewrite Rmult_assoc.
rewrite <- Rmult_plus_distr_l.
apply Rmult_le_compat_l.
left; prove_sup0.
rewrite <- Rmult_plus_distr_l.
rewrite (Rmult_comm (u0 t)); apply Rmult_le_compat_l.
left; apply (TypeSpeed_pos (h intr)).
generalize
 (sqrt_cauchy (cos (theta intr t)) (sin (theta intr t)) (xP t) (yP t));
 rewrite (Rplus_comm (Rsqr (cos (theta intr t)))); 
 rewrite sin2_cos2; rewrite sqrt_1; rewrite Rmult_1_l; 
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
 intro H8; unfold u0 in |- *; assumption.
set (H0 := xP_derivable t).
set (H1 := yP_derivable t).
(* Goal: derivable (fun t : R => Rmult (v vi) t) *)
symmetry  in |- *; reg.
unfold derive_pt in |- *; unfold derivable_pt_abs in |- *;
 cut
  (forall l : R,
   derivable_pt_lim (fun y : R => (Rsqr (xP y) + (Rsqr (yP y) + Rsqr eps))%R)
     t l <-> derivable_pt_lim (fun y : R => Rsqr (f y)) t l).
intro; unfold projT1 in |- *.
case (fct_der3 eps t); intros.
case (fct_der2 eps t); intros.
assert (H0 := H x).
unfold derivable_pt_abs in d.
elim H0; intros; fold f in d0.
assert (H3 := H1 d).
eapply uniqueness_limite.
apply H3.
apply d0.
intro; unfold derivable_pt_lim in |- *.
split; intros.
elim (H eps0 H0); intros.
exists x; intros; unfold f in |- *; unfold u in |- *.
repeat rewrite Rsqr_sqrt.
(* Goal: Rlt (Rplus (Rsqr (xP x)) (Rsqr (yP x))) (Rplus (Rplus (Rsqr (xP x)) (Rsqr (yP x))) (Rsqr (pos eps))) *)
repeat rewrite Rplus_assoc.
apply H1; assumption.
repeat apply Rplus_le_le_0_compat; try apply Rle_0_sqr.
repeat apply Rplus_le_le_0_compat; try apply Rle_0_sqr.
elim (H eps0 H0); intros.
exists x; intros; unfold f in H1; unfold u in H1.
replace
 ((Rsqr (xP (t + h)) + (Rsqr (yP (t + h)) + Rsqr eps) -
   (Rsqr (xP t) + (Rsqr (yP t) + Rsqr eps))) / h - l)%R with
 ((Rsqr (sqrt (Rsqr (xP (t + h)) + Rsqr (yP (t + h)) + Rsqr eps)) -
   Rsqr (sqrt (Rsqr (xP t) + Rsqr (yP t) + Rsqr eps))) / h - l)%R.
apply H1; assumption.
repeat rewrite Rsqr_sqrt.
repeat rewrite Rplus_assoc; reflexivity.
repeat apply Rplus_le_le_0_compat; try apply Rle_0_sqr.
repeat apply Rplus_le_le_0_compat; try apply Rle_0_sqr.
Qed.

(**********)
Lemma u_stric_pos : forall (eps : posreal) (t : R), (0 < u eps t)%R.
intros; unfold u in |- *; apply sqrt_lt_R0; apply Rplus_le_lt_0_compat;
 [ apply Rplus_le_le_0_compat; apply Rle_0_sqr
 | apply Rsqr_pos_lt; red in |- *; intro H; generalize (cond_pos eps);
    intro H0; rewrite H in H0; elim (Rlt_irrefl 0 H0) ].
Qed.

Lemma u_pos : forall (eps : posreal) (t : R), (0 <= u eps t)%R.
(* Goal: forall (eps : posreal) (t : R), Rle (IZR Z0) (u eps t) *)
intros; left; apply u_stric_pos.
Qed.

Lemma u0_pos : forall t : R, (0 <= u0 t)%R.
intros; unfold u0 in |- *; apply sqrt_positivity; apply Rplus_le_le_0_compat;
 apply Rle_0_sqr.
Qed.

(**********)
Lemma Rsqr_u_epsilon :
 forall (eps : posreal) (t : R), Rsqr (u eps t) = (Rsqr (u0 t) + Rsqr eps)%R.
intros; apply sqrt_inj;
 [ apply Rle_0_sqr
 | apply Rplus_le_le_0_compat; apply Rle_0_sqr
 | rewrite sqrt_Rsqr;
    [ unfold u0 in |- *; rewrite Rsqr_sqrt;
       [ unfold u in |- *; reflexivity
       | apply Rplus_le_le_0_compat; apply Rle_0_sqr ]
    | apply (u_pos eps t) ] ].
Qed.

(**********)
Lemma u0_u_epsilon : forall (eps : posreal) (t : R), (u0 t <= u eps t)%R.
intros; apply Rsqr_incr_0;
 [ unfold u0, u in |- *; repeat rewrite Rsqr_sqrt;
    [ rewrite <- (Rplus_0_r (Rsqr (xP t) + Rsqr (yP t)));
       repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l;
       rewrite Rplus_0_l; apply Rle_0_sqr
    | repeat apply Rplus_le_le_0_compat; apply Rle_0_sqr
    | apply Rplus_le_le_0_compat; apply Rle_0_sqr ]
 | apply u0_pos
 | apply u_pos ].
Qed.

(**********)
Lemma u_epsilon_le_v :
 forall (eps : posreal) (t : R), (derive_pt (u eps) t (d_u eps t) <= vi)%R.
(* Goal: forall (eps : posreal) (t : R) (_ : Rle (IZR Z0) t), Rle (Rminus (u eps t) (pos eps)) (Rmult (v vi) t) *)
intros.
(* Goal: Rle (derive_pt (u eps) t (d_u eps t)) (v vi) *)
generalize (D_Rsqr_u_epsilon_2 eps t); intro H.
(* Goal: Rle (derive_pt (u eps) t (d_u eps t)) (v vi) *)
rewrite (D_Rsqr_u_epsilon_1 eps t) in H.
(* Goal: Rle (derive_pt (u eps) t (d_u eps t)) (v vi) *)
repeat rewrite Rmult_assoc in H.
(* Goal: Rle (derive_pt (u eps) t (d_u eps t)) (v vi) *)
assert (Hyp : (0 < 2)%R).
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: Rlt (IZR Z0) (v vi) *)
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
prove_sup0.
generalize
 (Rmult_le_reg_l 2 (u eps t * derive_pt (u eps) t (d_u eps t)) 
(* Goal: forall _ : @eq R (u eps (IZR Z0)) (pos eps), Rle (Rminus (u eps t) (pos eps)) (Rmult (v vi) t) *)
(* Goal: @eq R (u eps (IZR Z0)) (pos eps) *)
    (u0 t * vi) Hyp H); intro H1.
generalize (u0_u_epsilon eps t); intro H2;
 generalize
  (Rmult_le_compat_r (v vi) (u0 t) (u eps t) (Rlt_le 0 vi (TypeSpeed_pos vi))
     H2); intro H3.
generalize
 (Rle_trans (u eps t * derive_pt (u eps) t (d_u eps t)) 
    (u0 t * vi) (u eps t * vi) H1 H3); intro H4.
apply
 (Rmult_le_reg_l (u eps t) (derive_pt (u eps) t (d_u eps t)) vi
    (u_stric_pos eps t) H4).
Qed.

(**********)
Lemma vit_derivable : derivable (fun t : R => (vi * t)%R).
(* Goal: derivable (fun t : R => Rmult (v vi) t) *)
reg.
Qed.

Lemma derive_vit :
 forall t : R, derive_pt (fun t : R => (vi * t)%R) t (vit_derivable t) = vi.
(* Goal: derivable (fun t : R => Rmult (v vi) t) *)
intro; reg.
Qed.

(**********)
Lemma u_epsilon_le_vt :
 forall (eps : posreal) (t : R), (0 <= t)%R -> (u eps t - eps <= vi * t)%R.
(* Goal: forall (eps : posreal) (t : R) (_ : Rle (IZR Z0) t), Rle (Rminus (u eps t) (pos eps)) (Rmult (v vi) t) *)
intros.
generalize
 (IAF_var (fun t : R => (vi * t)%R) (fun t : R => u eps t) 0 t vit_derivable
(* Goal: forall (eps : posreal) (t : R) (_ : Rle (IZR Z0) t), Rle (Rminus (u eps t) (pos eps)) (Rmult (v vi) t) *)
    (d_u eps) H); intros.
(* Goal: Rle (Rminus (u eps t) (pos eps)) (Rmult (v vi) t) *)
cut (u eps 0 = eps).
(* Goal: forall _ : @eq R (u eps (IZR Z0)) (pos eps), Rle (Rminus (u eps t) (pos eps)) (Rmult (v vi) t) *)
(* Goal: @eq R (u eps (IZR Z0)) (pos eps) *)
intro H1.
(* Goal: Rle (Rminus (u eps t) (pos eps)) (Rmult (v vi) t) *)
(* Goal: @eq R (u eps (IZR Z0)) (pos eps) *)
rewrite <- H1.
(* Goal: forall (eps : posreal) (t : R) (_ : Rle (IZR Z0) t), Rle (Rminus (u eps t) (pos eps)) (Rmult (v vi) t) *)
elim H0; intros.
rewrite Rmult_0_r in H2; unfold Rminus in H2; rewrite Ropp_0 in H2;
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
 rewrite Rplus_0_r in H2; left; assumption.
rewrite Rmult_0_r in H2; unfold Rminus in H2; rewrite Ropp_0 in H2;
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
 rewrite Rplus_0_r in H2; right; assumption.
(* Goal: Rle (derive_pt (fun t : R => u eps t) c (d_u eps c)) (derive_pt (fun t : R => Rmult (v vi) t) c (vit_derivable c)) *)
(* Goal: @eq R (u eps (IZR Z0)) (pos eps) *)
rewrite (derive_vit c); apply (u_epsilon_le_v eps c).
unfold u in |- *; unfold xP in |- *; unfold yP in |- *; unfold Rminus in |- *;
 repeat rewrite Rplus_opp_r; rewrite Rsqr_0; repeat rewrite Rplus_0_l;
 apply (sqrt_Rsqr eps (Rlt_le 0 eps (cond_pos eps))).
Qed.

(**********)
Lemma Rsqr_u :
 forall (eps : posreal) (t : R),
 (0 <= t)%R -> (Rsqr (u0 t) <= Rsqr vi * Rsqr t + 2 * eps * vi * t)%R.
(* Goal: forall (eps : posreal) (t : R) (_ : Rle (IZR Z0) t), Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) (pos eps)) (v vi)) t)) *)
intros; cut (u eps t <= vi * t + eps)%R.
intro H0; generalize (u_pos eps t); intro H1;
 generalize
  (Rsqr_incr_1 (u eps t) (vi * t + eps) H0 H1
     (Rle_trans 0 (u eps t) (vi * t + eps) H1 H0)); 
 intro H2; rewrite Rsqr_plus in H2; rewrite Rsqr_u_epsilon in H2;
 rewrite Rsqr_mult in H2; rewrite <- (Rplus_comm (2 * (vi * t) * eps)) in H2;
 generalize
  (Rplus_le_compat_r (- Rsqr eps) (Rsqr (u0 t) + Rsqr eps)
     (2 * (vi * t) * eps + (Rsqr vi * Rsqr t + Rsqr eps)) H2);
 unfold Rminus in |- *; repeat rewrite Rplus_assoc;
 repeat rewrite Rplus_opp_r; repeat rewrite Rplus_0_r; 
 intro H3;
 replace (Rsqr vi * Rsqr t + 2 * eps * vi * t)%R with
  (2 * (vi * t) * eps + Rsqr vi * Rsqr t)%R.
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
assumption.
(* Goal: @eq R (Rmult (Rmult (Rmult (pos eps) (Rmult (IZR (Zpos (xO xH))) (Rinv (IZR (Zpos (xO xH)))))) (Rmult (Rinv (v vi)) (v vi))) (Rmult (Rinv t) t)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) (Rmult (pos eps) (Rmult (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rinv (v vi))) (Rinv t)))) (v vi)) t) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: not (@eq R (Rmult (IZR (Zpos (xO xH))) (v vi)) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
ring.
apply Rplus_le_reg_l with (- eps)%R; rewrite Rplus_comm;
 replace (- eps + (vi * t + eps))%R with (vi * t)%R.
generalize (u_epsilon_le_vt eps t H); unfold Rminus in |- *; intro;
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
 assumption.
(* Goal: @eq R (Rmult (Rmult (Rmult (pos eps) (Rmult (IZR (Zpos (xO xH))) (Rinv (IZR (Zpos (xO xH)))))) (Rmult (Rinv (v vi)) (v vi))) (Rmult (Rinv t) t)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) (Rmult (pos eps) (Rmult (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rinv (v vi))) (Rinv t)))) (v vi)) t) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: not (@eq R (Rmult (IZR (Zpos (xO xH))) (v vi)) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
ring.
Qed.

(**********)
Lemma Rsqr_u_Rsqr_vt :
 forall (eps : posreal) (t : R),
 (0 <= t)%R -> (Rsqr (u0 t) <= Rsqr vi * Rsqr t + eps)%R.
(* Goal: forall eps : posreal, derivable (fun t : R => u eps t) *)
intros; case (Rtotal_order 0 t); intro.
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
cut (0 < eps / (2 * vi * t))%R.
intro; generalize (Rsqr_u (mkposreal (eps / (2 * vi * t)) H1) t H);
 simpl in |- *;
 replace (2 * (eps / (2 * vi * t)) * vi * t)%R with (eps * 1)%R.
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
rewrite Rmult_1_r; intro; assumption.
(* Goal: @eq R (Rmult (pos eps) (IZR (Zpos xH))) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t))) (v vi)) t) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
unfold Rdiv in |- *; repeat rewrite Rinv_mult_distr.
replace (2 * (eps * (/ 2 * / vi * / t)) * vi * t)%R with
 (eps * (2 * / 2) * (/ vi * vi) * (/ t * t))%R.
(* Goal: @eq R (Rmult (pos eps) (IZR (Zpos xH))) (Rmult (Rmult (Rmult (pos eps) (Rmult (IZR (Zpos (xO xH))) (Rinv (IZR (Zpos (xO xH)))))) (Rmult (Rinv (v vi)) (v vi))) (Rmult (Rinv t) t)) *)
(* Goal: @eq R (Rmult (Rmult (Rmult (pos eps) (Rmult (IZR (Zpos (xO xH))) (Rinv (IZR (Zpos (xO xH)))))) (Rmult (Rinv (v vi)) (v vi))) (Rmult (Rinv t) t)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) (Rmult (pos eps) (Rmult (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rinv (v vi))) (Rinv t)))) (v vi)) t) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: not (@eq R (Rmult (IZR (Zpos (xO xH))) (v vi)) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
repeat rewrite <- Rinv_l_sym.
(* Goal: @eq R (Rmult (pos eps) (IZR (Zpos xH))) (Rmult (Rmult (Rmult (pos eps) (Rmult (IZR (Zpos (xO xH))) (Rinv (IZR (Zpos (xO xH)))))) (IZR (Zpos xH))) (IZR (Zpos xH))) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: @eq R (Rmult (Rmult (Rmult (pos eps) (Rmult (IZR (Zpos (xO xH))) (Rinv (IZR (Zpos (xO xH)))))) (Rmult (Rinv (v vi)) (v vi))) (Rmult (Rinv t) t)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) (Rmult (pos eps) (Rmult (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rinv (v vi))) (Rinv t)))) (v vi)) t) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: not (@eq R (Rmult (IZR (Zpos (xO xH))) (v vi)) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
rewrite <- Rinv_r_sym.
(* Goal: @eq R (Rmult (pos eps) (IZR (Zpos xH))) (Rmult (Rmult (Rmult (pos eps) (IZR (Zpos xH))) (IZR (Zpos xH))) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: @eq R (Rmult (Rmult (Rmult (pos eps) (Rmult (IZR (Zpos (xO xH))) (Rinv (IZR (Zpos (xO xH)))))) (Rmult (Rinv (v vi)) (v vi))) (Rmult (Rinv t) t)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) (Rmult (pos eps) (Rmult (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rinv (v vi))) (Rinv t)))) (v vi)) t) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: not (@eq R (Rmult (IZR (Zpos (xO xH))) (v vi)) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
repeat rewrite Rmult_1_r; reflexivity.
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
discrR.
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
red in |- *; intro H2; rewrite H2 in H0; elim (Rlt_irrefl 0 H0).
generalize (TypeSpeed_pos vi); intro H2; red in |- *; intro H3;
 rewrite H3 in H2; elim (Rlt_irrefl 0 H2).
(* Goal: @eq R (Rmult (Rmult (Rmult (pos eps) (Rmult (IZR (Zpos (xO xH))) (Rinv (IZR (Zpos (xO xH)))))) (Rmult (Rinv (v vi)) (v vi))) (Rmult (Rinv t) t)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) (Rmult (pos eps) (Rmult (Rmult (Rinv (IZR (Zpos (xO xH)))) (Rinv (v vi))) (Rinv t)))) (v vi)) t) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: not (@eq R (Rmult (IZR (Zpos (xO xH))) (v vi)) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
ring.
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
discrR.
generalize (TypeSpeed_pos vi); intro H2; red in |- *; intro H3;
 rewrite H3 in H2; elim (Rlt_irrefl 0 H2).
(* Goal: not (@eq R (Rmult (IZR (Zpos (xO xH))) (v vi)) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
apply prod_neq_R0.
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: not (@eq R (v vi) (IZR Z0)) *)
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
discrR.
generalize (TypeSpeed_pos vi); intro H2; red in |- *; intro H3;
 rewrite H3 in H2; elim (Rlt_irrefl 0 H2).
(* Goal: not (@eq R t (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
red in |- *; intro H2; rewrite H2 in H0; elim (Rlt_irrefl 0 H0).
(* Goal: Rlt (IZR Z0) (Rdiv (pos eps) (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
unfold Rdiv in |- *; apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) (pos eps) *)
(* Goal: Rlt (IZR Z0) (Rinv (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
apply (cond_pos eps).
(* Goal: Rlt (IZR Z0) (Rinv (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
apply Rinv_0_lt_compat; repeat apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: Rlt (IZR Z0) (v vi) *)
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
prove_sup0.
(* Goal: Rlt (IZR Z0) (v vi) *)
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
apply (TypeSpeed_pos vi).
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
assumption.
(* Goal: forall eps : posreal, derivable (fun t : R => u eps t) *)
elim H0; intro.
rewrite <- H1; unfold u0 in |- *; unfold xP, yP in |- *;
 unfold Rminus in |- *; repeat rewrite Rplus_opp_r; 
 repeat rewrite Rsqr_0; rewrite Rmult_0_r; repeat rewrite Rplus_0_l;
(* Goal: Rlt (IZR Z0) (pos eps) *)
(* Goal: Rlt (IZR Z0) (Rinv (Rmult (Rmult (IZR (Zpos (xO xH))) (v vi)) t)) *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
 rewrite sqrt_0; rewrite Rsqr_0; left; apply (cond_pos eps).
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
elim (Rlt_irrefl 0 (Rle_lt_trans 0 t 0 H H1)).
Qed.

(**********************)
(****** THEOREM *******)
(**********************)

Theorem YCNGFTYS :
 forall t : R,
 (0 <= t)%R -> (sqrt (Rsqr (xi t - xi 0) + Rsqr (yi t - yi 0)) <= v vi * t)%R.
(* Goal: forall (t : R) (_ : Rle (IZR Z0) t), Rle (sqrt (Rplus (Rsqr (Rminus (xi t) (xi (IZR Z0)))) (Rsqr (Rminus (yi t) (yi (IZR Z0)))))) (Rmult (v vi) t) *)
intros; apply Rsqr_incr_0.
rewrite Rsqr_mult; apply le_epsilon; intros;
 generalize (Rsqr_u_Rsqr_vt (mkposreal eps H0) t H); 
 simpl in |- *; unfold u0 in |- *; unfold xP, yP in |- *; 
(* Goal: Rlt (IZR Z0) t *)
(* Goal: Rle (Rsqr (u0 t)) (Rplus (Rmult (Rsqr (v vi)) (Rsqr t)) (pos eps)) *)
 intro H1; assumption.
(* Goal: Rle (IZR Z0) (Rplus (Rsqr (xP x)) (Rsqr (yP x))) *)
(* Goal: Rlt (Rplus (Rsqr (xP x)) (Rsqr (yP x))) (Rplus (Rplus (Rsqr (xP x)) (Rsqr (yP x))) (Rsqr (pos eps))) *)
apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr.
(* Goal: Rle (IZR Z0) (Rmult (v vi) t) *)
apply Rmult_le_pos; [ left; apply (TypeSpeed_pos vi) | assumption ].
Qed.

End ycngftys.
