# Library AILS.trajectory

Section trajectory.

Require Import Bool.
Require Import Reals.
Require Import trajectory_const.
Require Import rrho.
Require Import trajectory_def.
Require Import constants.
Require Import ycngftys.
Require Import ycngstys.
Require Import Omega.

Variable intr : Trajectory.
Variable T : TimeT.

Lemma thetat_derivable : derivable (thetat intr).
unfold thetat in |- *; apply (cond_diff (theta intr)).
Qed.

Definition xe : R := x (tr evad) T.
Definition ye : R := y (tr evad) T.
Definition ve : R := v (h (tr evad)).
Definition r_vi : R := r (vi intr).
Definition rho_vi : R := rho (vi intr).
Definition Die (ti te : R) : R :=
sqrt
(Rsqr (xi intr ti - x (tr evad) te) + Rsqr (yi intr ti - y (tr evad) te)).
Definition conflict (t : R) : bool :=
match Rle_dec (Die t t) ConflictRange with
| left _true
| right _false
end.

Lemma Dx :
t : R,
derive_pt (xi intr) t (xi_derivable intr t) =
(vi intr × cos (thetat intr t))%R.
intro; unfold xi, vi, thetat in |- ×.
assert (H := cond_x intr t).
rewrite <- H.
apply pr_nu.
Qed.

Lemma Dy :
t : R,
derive_pt (yi intr) t (yi_derivable intr t) =
(vi intr × sin (thetat intr t))%R.
intro; unfold yi, vi, thetat in |- ×.
assert (H := cond_y intr t).
rewrite <- H.
apply pr_nu.
Qed.

Axiom r_sin_rho : (ConflictRange < r_vi × sin rho_vi)%R.

Definition l : R := Die 0 T.
Definition d : R := Die 0 0.

Axiom
beta_exists :
{ beta : R |
xe = (l × cos beta + xi intr 0)%R
ye = (yi intr 0 - l × sin beta)%R
(0 beta + thetat intr 0 < 2 × PI)%R }.

Definition beta := let (a,_) := beta_exists in a.

Lemma beta_def :
xe = (l × cos beta + xi intr 0)%R
ye = (yi intr 0 - l × sin beta)%R (0 beta + thetat intr 0 < 2 × PI)%R.
unfold beta in |- *; case beta_exists; trivial.
Qed.

Definition Omega (a : R) : bool :=
match Rle_dec (PI / 2) a with
| left _
match Rle_dec a (3 × (PI / 2)) with
| left _true
| right _false
end
| right _false
end.

Lemma xe_0 : xe = (l × cos beta + xi intr 0)%R.
Proof with trivial.
generalize beta_def; intro; elim H...
Qed.

Lemma ye_0 : ye = (yi intr 0 - l × sin beta)%R.
Proof with trivial.
generalize beta_def; intro; elim H; intros _ H0; elim H0...
Qed.

Lemma d_l_beta :
Rsqr d = (Rsqr (ve × T) + Rsqr l - 2 × ve × T × l × cos beta)%R.
Proof with trivial.
unfold d in |- *; unfold Die in |- *; rewrite Rsqr_sqrt...
replace (xi intr 0 - x (tr evad) 0)%R with
(xi intr 0 - xe + (xe - x (tr evad) 0))%R...
replace (yi intr 0 - y (tr evad) 0)%R with
(yi intr 0 - ye + (ye - y (tr evad) 0))%R...
repeat rewrite Rsqr_plus; cut ((ye - y (tr evad) 0)%R = 0%R)...
intro; rewrite H; repeat rewrite Rmult_0_r; rewrite Rsqr_0;
repeat rewrite Rplus_0_r; cut ((xe - x (tr evad) 0)%R = (ve × T)%R)...
intro; rewrite H0;
replace
(Rsqr (xi intr 0 - xe) + Rsqr (ve × T) + 2 × (xi intr 0 - xe) × (ve × T) +
Rsqr (yi intr 0 - ye))%R with
(Rsqr (ve × T) + (Rsqr (xi intr 0 - xe) + Rsqr (yi intr 0 - ye)) +
2 × (xi intr 0 - xe) × (ve × T))%R...
cut (Rsqr l = (Rsqr (xi intr 0 - xe) + Rsqr (yi intr 0 - ye))%R)...
intro; rewrite <- H1; rewrite xe_0; ring...
unfold l in |- *; unfold Die in |- *; rewrite Rsqr_sqrt;
[ unfold xe, ye in |- × | apply Rplus_le_le_0_compat; apply Rle_0_sqr ]...
ring...
unfold xe, ve in |- *; rewrite (tr_cond1 evad); ring...
unfold ye, ve in |- *; rewrite (tr_cond2 evad); unfold Rminus in |- *;
rewrite Rplus_opp_r...
ring...
ring...
apply Rplus_le_le_0_compat; apply Rle_0_sqr...
Qed.

Definition yp (t : R) : R :=
(- sin (thetat intr 0) × (xi intr t - xe) +
cos (thetat intr 0) × (yi intr t - ye))%R.

Hint Resolve xi_derivable yi_derivable: diff.

Lemma yp_derivable : derivable yp.
unfold yp in |- *; set (thetat_p := thetat intr); set (xi_p := xi intr);
set (yi_p := yi intr); reg.
apply (yi_derivable intr).
apply (xi_derivable intr).
Qed.
Hint Resolve yp_derivable: diff.

Definition xp (t : R) : R :=
(cos (thetat intr 0) × (xi intr t - xe) +
sin (thetat intr 0) × (yi intr t - ye))%R.

Lemma xp_derivable : derivable xp.
unfold xp in |- *; set (thetat_p := thetat intr); set (xi_p := xi intr);
set (yi_p := yi intr); reg.
apply (yi_derivable intr).
apply (xi_derivable intr).
Qed.
Hint Resolve xp_derivable: diff.

Definition Rsqr_evader_distance (t : R) : R :=
(Rsqr (xi intr t - xe) + Rsqr (yi intr t - ye))%R.

unfold Rsqr_evader_distance in |- ×.
set (xi_p := xi intr); set (yi_p := yi intr); reg.
apply (yi_derivable intr).
apply (xi_derivable intr).
Qed.
Hint Resolve Rsqr_evader_distance_derivable: diff.

Definition Rsqr_intruder_distance (t : R) : R :=
(Rsqr (xi intr t - xi intr 0) + Rsqr (yi intr t - yi intr 0))%R.

Lemma Rsqr_intruder_distance_derivable : derivable Rsqr_intruder_distance.
unfold Rsqr_intruder_distance in |- *; set (xi_p := xi intr);
set (yi_p := yi intr); reg.
apply (yi_derivable intr).
apply (xi_derivable intr).
Qed.
Hint Resolve Rsqr_intruder_distance_derivable: diff.

t : R, (0 Rsqr_evader_distance t)%R.
intro; unfold Rsqr_evader_distance in |- *; apply Rplus_le_le_0_compat;
apply Rle_0_sqr.
Qed.

Lemma Rsqr_intruder_distance_pos :
t : R, (0 Rsqr_intruder_distance t)%R.
intro; unfold Rsqr_intruder_distance in |- *; apply Rplus_le_le_0_compat;
apply Rle_0_sqr.
Qed.

Definition e (t : R) : R := sqrt (Rsqr_evader_distance t).
Definition i (t : R) : R := sqrt (Rsqr_intruder_distance t).

Lemma conflict_T_e_0 : conflict T = true (e T ConflictRange)%R.
Proof with trivial.
unfold conflict in |- *; cut (e T = Die T T)...
intro; case (Rle_dec (Die T T) ConflictRange); intros;
[ rewrite H; exact r | elim diff_false_true ]...
Qed.

Lemma conflict_T_e_1 : (e T ConflictRange)%R conflict T = true.
Proof with trivial.
intro; cut (e T = Die T T)...
intro; rewrite H0 in H; unfold conflict in |- *;
case (Rle_dec (Die T T) ConflictRange); intro...
elim n; assumption...
Qed.

Lemma L : Rsqr l = (Rsqr (xe - xi intr 0) + Rsqr (ye - yi intr 0))%R.
rewrite xe_0; rewrite ye_0; unfold Rminus in |- *;
rewrite <- (Rplus_comm (- (l × sin beta))); repeat rewrite Rplus_assoc;
repeat rewrite Rplus_opp_r; repeat rewrite Rplus_0_r;
rewrite <- Rsqr_neg; repeat rewrite Rsqr_mult;
rewrite <- (Rmult_comm (Rsqr (sin beta))); rewrite sin2;
unfold Rminus in |- *; rewrite Rmult_plus_distr_r;
ring.
Qed.

Lemma L_intruder : t : R, (l e t + i t)%R.
intro; apply Rsqr_incr_0.
rewrite Rsqr_plus.
cut
(Rsqr l =
(Rsqr (e t) + Rsqr (i t) +
2 ×
((xe - xi intr t) × (xi intr t - xi intr 0) +
(ye - yi intr t) × (yi intr t - yi intr 0)))%R).
intro.
rewrite H.
apply Rplus_le_compat_l.
repeat rewrite Rmult_assoc.
apply Rmult_le_compat_l.
left; prove_sup0.
unfold e, i in |- ×.
unfold Rsqr_evader_distance, Rsqr_intruder_distance in |- ×.
rewrite (Rsqr_neg (xi intr t - xe)).
rewrite (Rsqr_neg (yi intr t - ye)).
replace (- (xi intr t - xe))%R with (xe - xi intr t)%R.
replace (- (yi intr t - ye))%R with (ye - yi intr t)%R.
apply sqrt_cauchy.
ring.
ring.
rewrite L.
unfold e, i in |- ×.
repeat rewrite Rsqr_sqrt.
unfold Rsqr_evader_distance, Rsqr_intruder_distance in |- ×.
replace (xe - xi intr 0)%R with (xe - xi intr t + (xi intr t - xi intr 0))%R.
replace (ye - yi intr 0)%R with (ye - yi intr t + (yi intr t - yi intr 0))%R.
repeat rewrite Rsqr_plus.
rewrite (Rsqr_neg (xe - xi intr t)).
rewrite (Rsqr_neg (ye - yi intr t)).
replace (- (xe - xi intr t))%R with (xi intr t - xe)%R.
replace (- (ye - yi intr t))%R with (yi intr t - ye)%R.
ring.
ring.
ring.
ring.
ring.
apply Rsqr_intruder_distance_pos.
unfold l in |- *; unfold Die in |- ×.
apply sqrt_positivity.
apply Rplus_le_le_0_compat; apply Rle_0_sqr.
unfold e, i in |- *; apply Rplus_le_le_0_compat; apply sqrt_positivity.
apply Rsqr_intruder_distance_pos.
Qed.

Lemma l_is_pos : (0 l)%R.
unfold l in |- *; unfold Die in |- *; apply sqrt_positivity;
apply Rplus_le_le_0_compat; apply Rle_0_sqr.
Qed.

Lemma L_e : t : R, (e t l + i t)%R.
intro.
apply Rsqr_incr_0.
rewrite Rsqr_plus.
cut
(Rsqr (e t) =
(Rsqr l + Rsqr (i t) +
2 ×
((xi intr t - xi intr 0) × (xi intr 0 - xe) +
(yi intr t - yi intr 0) × (yi intr 0 - ye)))%R).
intro.
rewrite H.
apply Rplus_le_compat_l.
repeat rewrite Rmult_assoc.
apply Rmult_le_compat_l.
left; prove_sup0.
cut (l = sqrt (Rsqr (xe - xi intr 0) + Rsqr (ye - yi intr 0))).
intro.
rewrite H0.
unfold i in |- ×.
unfold Rsqr_intruder_distance in |- ×.
rewrite (Rsqr_neg (xe - xi intr 0)).
rewrite (Rsqr_neg (ye - yi intr 0)).
replace (- (xe - xi intr 0))%R with (xi intr 0 - xe)%R.
replace (- (ye - yi intr 0))%R with (yi intr 0 - ye)%R.
rewrite <-
(Rmult_comm
(sqrt (Rsqr (xi intr t - xi intr 0) + Rsqr (yi intr t - yi intr 0))))
.
apply sqrt_cauchy.
ring.
ring.
apply Rsqr_inj.
apply l_is_pos.
apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr.
rewrite Rsqr_sqrt.
apply L.
apply Rplus_le_le_0_compat; apply Rle_0_sqr.
rewrite L.
unfold e, i in |- ×.
repeat rewrite Rsqr_sqrt.
unfold Rsqr_evader_distance, Rsqr_intruder_distance in |- ×.
replace (xi intr t - xe)%R with (xi intr t - xi intr 0 + (xi intr 0 - xe))%R.
replace (yi intr t - ye)%R with (yi intr t - yi intr 0 + (yi intr 0 - ye))%R.
repeat rewrite Rsqr_plus.
rewrite (Rsqr_neg (xe - xi intr 0)).
rewrite (Rsqr_neg (ye - yi intr 0)).
replace (- (xe - xi intr 0))%R with (xi intr 0 - xe)%R.
replace (- (ye - yi intr 0))%R with (yi intr 0 - ye)%R.
ring.
ring.
ring.
ring.
ring.
apply Rsqr_intruder_distance_pos.
unfold e in |- ×.
apply sqrt_positivity.
apply Rplus_le_le_0_compat.
apply l_is_pos.
unfold i in |- ×.
apply sqrt_positivity.
apply Rsqr_intruder_distance_pos.
Qed.

Lemma L_i : t : R, (i t l + e t)%R.
intro.
apply Rsqr_incr_0.
rewrite Rsqr_plus.
cut
(Rsqr (i t) =
(Rsqr l + Rsqr (e t) +
2 ×
((xi intr t - xe) × (xe - xi intr 0) + (yi intr t - ye) × (ye - yi intr 0)))%R).
intro.
rewrite H.
apply Rplus_le_compat_l.
repeat rewrite Rmult_assoc.
apply Rmult_le_compat_l.
left; prove_sup0.
cut (l = sqrt (Rsqr (xe - xi intr 0) + Rsqr (ye - yi intr 0))).
intro.
rewrite H0.
unfold e in |- ×.
unfold Rsqr_evader_distance in |- ×.
rewrite <-
(Rmult_comm (sqrt (Rsqr (xi intr t - xe) + Rsqr (yi intr t - ye))))
.
apply sqrt_cauchy.
apply Rsqr_inj.
apply l_is_pos.
apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr.
rewrite Rsqr_sqrt.
apply L.
apply Rplus_le_le_0_compat; apply Rle_0_sqr.
rewrite L.
unfold e, i in |- ×.
repeat rewrite Rsqr_sqrt.
unfold Rsqr_evader_distance, Rsqr_intruder_distance in |- ×.
replace (xi intr t - xi intr 0)%R with (xi intr t - xe + (xe - xi intr 0))%R.
replace (yi intr t - yi intr 0)%R with (yi intr t - ye + (ye - yi intr 0))%R.
repeat rewrite Rsqr_plus.
ring.
ring.
ring.
apply Rsqr_intruder_distance_pos.
unfold i in |- ×.
apply sqrt_positivity.
apply Rsqr_intruder_distance_pos.
apply Rplus_le_le_0_compat.
apply l_is_pos.
unfold e in |- ×.
apply sqrt_positivity.
Qed.

Lemma theta_inv :
t : R,
(0 t)%R
(thetat intr 0 - rho_vi × t thetat intr t)%R
(thetat intr t thetat intr 0 + rho_vi × t)%R.
Proof with trivial.
generalize (dtheta_rho intr); intros; split...
unfold thetat in |- *; cut (derivable (fun y : R ⇒ (- rho_vi × y)%R));
[ intro X | reg ]...
cut
( z : R,
derive_pt (fun y : R ⇒ (- rho_vi × y)%R) z (X z) = (- rho_vi)%R);
[ intro | intro; reg ]...
apply Rplus_le_reg_l with (- theta intr 0)%R...
replace (- theta intr 0 + (theta intr 0 - rho_vi × t))%R with
(- rho_vi × t - - rho_vi × 0)%R; [ idtac | ring ]...
replace (- theta intr 0 + theta intr t)%R with
(theta intr t - theta intr 0)%R; [ idtac | ring ]...
apply
(IAF_var (theta intr) (fun y : R ⇒ (- rho_vi × y)%R) 0 t
(cond_diff (theta intr)) X H0)...
intros; rewrite (H1 c); unfold rho_vi in |- *; unfold vi in |- *; elim (H c);
intros H4 _; assumption...
unfold thetat in |- *; cut (derivable (fun y : R ⇒ (rho_vi × y)%R));
[ intro X | reg ]...
cut ( z : R, derive_pt (fun y : R ⇒ (rho_vi × y)%R) z (X z) = rho_vi);
[ intro | intro; reg ]...
apply Rplus_le_reg_l with (- theta intr 0)%R...
replace (- theta intr 0 + (theta intr 0 + rho_vi × t))%R with
(rho_vi × t - rho_vi × 0)%R; [ idtac | ring ]...
replace (- theta intr 0 + theta intr t)%R with
(theta intr t - theta intr 0)%R; [ idtac | ring ]...
apply
(IAF_var (fun y : R ⇒ (rho_vi × y)%R) (theta intr) 0 t X
(cond_diff (theta intr)) H0)...
intros; rewrite (H1 c); unfold rho_vi in |- *; unfold vi in |- *; elim (H c)...
Qed.

Lemma rho_t_pos : t : R, (0 t)%R (0 rho_vi × t)%R.
Proof with trivial.
intros; apply Rmult_le_pos...
left; unfold rho_vi in |- *; apply rho_pos...
Qed.

Lemma rho_t_le :
t1 t2 : R, (t1 t2)%R (rho_vi × t1 rho_vi × t2)%R.
Proof with trivial.
intros; apply Rmult_le_compat_l...
left; unfold rho_vi in |- *; apply rho_pos...
Qed.

Lemma Dyp :
t : R,
derive_pt yp t (yp_derivable t) =
(v (vi intr) × sin (thetat intr t - thetat intr 0))%R.
intro; unfold yp in |- ×.
assert (H := xi_derivable intr t).
assert (H0 := yi_derivable intr t).
assert (H1 := thetat_derivable t).
set (xi_p := xi intr) in H |- ×.
set (yi_p := yi intr) in H0 |- ×.
set (thetat_p := thetat intr) in H1 |- ×.
reg.
assert (H2 := cond_x intr t).
assert (H3 := cond_y intr t).
replace (derive_pt xi_p t H) with
(derive_pt (x intr) t (cond_diff (x intr) t)); [ idtac | apply pr_nu ].
replace (derive_pt yi_p t H0) with
(derive_pt (y intr) t (cond_diff (y intr) t)); [ idtac | apply pr_nu ].
rewrite H2; rewrite H3.
rewrite sin_minus.
unfold fct_cte, vi, thetat_p, thetat in |- ×.
ring.
Qed.

Lemma Dyp0_PI2 :
t : R,
(0 t)%R
(rho_vi × t PI / 2)%R
(- (vi intr × sin (rho_vi × t)) derive_pt yp t (yp_derivable t)
vi intr × sin (rho_vi × t))%R.
Proof with trivial.
intros...
rewrite Dyp...
generalize (theta_inv t H); intro; elim H1; intros...
cut (thetat intr t - thetat intr 0 rho_vi × t)%R...
cut (- (rho_vi × t) thetat intr t - thetat intr 0)%R...
intros...
split...
replace (- (vi intr × sin (rho_vi × t)))%R with
(vi intr × - sin (rho_vi × t))%R...
apply Rmult_le_compat_l...
left; apply TypeSpeed_pos...
rewrite <- (sin_neg (rho_vi × t))...
apply sin_incr_1...
apply Ropp_ge_le_contravar; apply Rle_ge...
apply Rle_trans with 0%R...
rewrite <- Ropp_0...
apply Ropp_ge_le_contravar; apply Rle_ge; apply (rho_t_pos t H)...
left; apply PI2_RGT_0...
apply Rle_trans with (- (rho_vi × t))%R...
apply Ropp_ge_le_contravar...
apply Rle_ge...
apply Rle_trans with (rho_vi × t)%R...
ring...
apply Rmult_le_compat_l...
left; apply TypeSpeed_pos...
apply sin_incr_1...
apply Rle_trans with (- (rho_vi × t))%R...
apply Ropp_ge_le_contravar; apply Rle_ge...
apply Rle_trans with (rho_vi × t)%R...
apply Rle_trans with 0%R...
rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; left;
apply PI2_RGT_0...
apply (rho_t_pos t H)...
apply Rplus_le_reg_l with (thetat intr 0)...
unfold Rminus in |- ×...
rewrite (Rplus_comm (thetat intr t))...
repeat rewrite <- Rplus_assoc...
rewrite Rplus_opp_r...
rewrite Rplus_0_l...
apply Rplus_le_reg_l with (thetat intr 0)...
unfold Rminus in |- ×...
rewrite (Rplus_comm (thetat intr t))...
repeat rewrite <- Rplus_assoc...
rewrite Rplus_opp_r...
rewrite Rplus_0_l...
Qed.

Lemma yp0 : yp 0 = (l × sin (thetat intr 0 + beta))%R.
unfold yp in |- *; rewrite xe_0; rewrite ye_0;
rewrite <- (Rplus_comm (xi intr 0)); unfold Rminus in |- *;
repeat rewrite Ropp_plus_distr; repeat rewrite <- Rplus_assoc;
repeat rewrite Rplus_opp_r; repeat rewrite Rplus_0_l;
rewrite sin_plus; ring.
Qed.

Definition hy (t : R) : R := (r_vi × cos (rho_vi × t))%R.

Lemma hy_derivable : derivable hy.
unfold hy in |- *; reg.
Qed.

Lemma Dhy :
t : R,
derive_pt hy t (hy_derivable t) = (- vi intr × sin (rho_vi × t))%R.
Proof with trivial.
intro; unfold hy in |- *; reg...
replace (vi intr:R) with (r_vi × rho_vi)%R.
ring.
unfold rho_vi, r_vi in |- *; unfold r in |- ×.
field.
assert (H := rho_pos (vi intr)); red in |- *; intro; rewrite H0 in H;
elim (Rlt_irrefl _ H)...
Qed.

Lemma ypt :
t : R,
(0 t)%R
(rho_vi × t PI / 2)%R (hy t - hy 0 yp t - yp 0 hy 0 - hy t)%R.
Proof with trivial.
intros; split...
apply (IAF_var yp hy 0 t yp_derivable hy_derivable H)...
intros; elim H1; intros...
generalize
(Dyp0_PI2 c H2
(Rle_trans (rho_vi × c) (rho_vi × t) (PI / 2) (rho_t_le c t H3) H0));
intro...
elim H4; intros...
cut (derive_pt hy c (hy_derivable c) = (- (vi intr × sin (rho_vi × c)))%R)...
intro...
rewrite <- H7 in H5...
rewrite Dhy; ring...
replace (hy 0 - hy t)%R with ((- hy)%F t - (- hy)%F 0)%R...
apply
(IAF_var (- hy)%F yp 0 t (derivable_opp hy hy_derivable) yp_derivable H)...
intros; elim H1; intros...
generalize
(Dyp0_PI2 c H2
(Rle_trans (rho_vi × c) (rho_vi × t) (PI / 2) (rho_t_le c t H3) H0));
intro...
elim H4; intros...
cut ((- derive_pt hy c (hy_derivable c))%R = (vi intr × sin (rho_vi × c))%R)...
intro; rewrite <- H7 in H6...
replace (derive_pt (- hy) c (derivable_opp hy hy_derivable c)) with
(derive_pt (- hy) c (derivable_pt_opp hy c (hy_derivable c)));
[ idtac | apply pr_nu ]...
rewrite (derive_pt_opp hy c (hy_derivable c))...
rewrite Dhy; ring...
unfold opp_fct in |- *; ring...
Qed.

Lemma ypt_PI2 :
t : R,
(0 t)%R
(rho_vi × t PI / 2)%R
(l × sin (beta + thetat intr 0) + r_vi × (cos (rho_vi × t) - 1) yp t)%R
(yp t l × sin (beta + thetat intr 0) - r_vi × (cos (rho_vi × t) - 1))%R.
intros; generalize (ypt t H H0); intro; elim H1; intros; split;
[ unfold hy in H2; unfold Rminus in H2; rewrite yp0 in H2;
rewrite Rmult_0_r in H2; rewrite cos_0 in H2; rewrite Rmult_1_r in H2;
generalize
(Rplus_le_compat_r (l × sin (thetat intr 0 + beta))
(r_vi × cos (rho_vi × t) + - r_vi)
(yp t + - (l × sin (thetat intr 0 + beta))) H2);
replace (r_vi × cos (rho_vi × t) + - r_vi)%R with
(r_vi × (cos (rho_vi × t) - 1))%R;
[ repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
intro; rewrite <- (Rplus_comm (r_vi × (cos (rho_vi × t) - 1)));
rewrite (Rplus_comm beta); assumption
| ring ]
| unfold hy in H3; unfold Rminus in H3; rewrite yp0 in H3;
rewrite Rmult_0_r in H3; rewrite cos_0 in H3; rewrite Rmult_1_r in H3;
generalize
(Rplus_le_compat_r (l × sin (thetat intr 0 + beta))
(yp t + - (l × sin (thetat intr 0 + beta)))
(r_vi + - (r_vi × cos (rho_vi × t))) H3);
replace (r_vi + - (r_vi × cos (rho_vi × t)))%R with
(- (r_vi × (cos (rho_vi × t) - 1)))%R;
[ repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
intro; unfold Rminus in |- *; rewrite (Rplus_comm beta);
rewrite <- (Rplus_comm (- (r_vi × (cos (rho_vi × t) + -1))));
assumption
| unfold Rminus in |- *; rewrite Rmult_plus_distr_l; ring ] ].
Qed.

Lemma Dxp :
t : R,
derive_pt xp t (xp_derivable t) =
(vi intr × cos (thetat intr t - thetat intr 0))%R.
intro; unfold xp in |- ×.
assert (H := xi_derivable intr t).
assert (H0 := yi_derivable intr t).
assert (H1 := thetat_derivable t).
set (xi_p := xi intr) in H |- ×.
set (yi_p := yi intr) in H0 |- ×.
set (thetat_p := thetat intr) in H1 |- ×.
reg.
assert (H2 := cond_x intr t).
assert (H3 := cond_y intr t).
replace (derive_pt yi_p t H0) with
(derive_pt (y intr) t (cond_diff (y intr) t)); [ idtac | apply pr_nu ].
replace (derive_pt xi_p t H) with
(derive_pt (x intr) t (cond_diff (x intr) t)); [ idtac | apply pr_nu ].
unfold vi in |- ×.
rewrite H2; rewrite H3; rewrite cos_minus; unfold thetat_p, thetat; ring.
Qed.

Lemma Dx0_PI :
t : R,
(0 t)%R
(rho_vi × t PI)%R
(vi intr × cos (rho_vi × t) derive_pt xp t (xp_derivable t))%R.
intros; rewrite Dxp; apply Rmult_le_compat_l;
[ left; apply TypeSpeed_pos
| generalize (theta_inv t H); intro; elim H1; intros;
case (Rcase_abs (thetat intr t - thetat intr 0));
intro;
[ cut (thetat intr 0 - thetat intr t rho_vi × t)%R;
[ cut (- (rho_vi × t) thetat intr 0 - thetat intr t)%R;
[ intros; rewrite <- (cos_neg (thetat intr t - thetat intr 0));
replace (- (thetat intr t - thetat intr 0))%R with
(thetat intr 0 - thetat intr t)%R;
[ apply cos_decr_1;
[ left;
generalize
(Ropp_lt_gt_contravar (thetat intr t - thetat intr 0) 0 r);
rewrite Ropp_0;
replace (- (thetat intr t - thetat intr 0))%R with
(thetat intr 0 - thetat intr t)%R;
[ intro; assumption | ring ]
| apply Rle_trans with (rho_vi × t)%R; assumption
| apply (rho_t_pos t H)
| assumption
| assumption ]
| ring ]
| apply Rplus_le_reg_l with (thetat intr t + rho_vi × t)%R;
repeat rewrite Rplus_assoc; rewrite Rplus_opp_r;
rewrite Rplus_0_r;
replace
(thetat intr t + (rho_vi × t + (thetat intr 0 - thetat intr t)))%R
with (thetat intr 0 + rho_vi × t)%R;
[ assumption | ring ] ]
| apply Rplus_le_reg_l with (thetat intr t - rho_vi × t)%R;
unfold Rminus in |- *; repeat rewrite Rplus_assoc;
rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite Rplus_comm;
repeat rewrite Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_r; rewrite Rplus_comm; assumption ]
| generalize (Rge_le (thetat intr t - thetat intr 0) 0 r); intro;
cut (thetat intr t - thetat intr 0 rho_vi × t)%R;
[ cut (- (rho_vi × t) thetat intr t - thetat intr 0)%R;
[ intros; apply cos_decr_1;
[ assumption
| apply Rle_trans with (rho_vi × t)%R; assumption
| apply (rho_t_pos t H)
| assumption
| assumption ]
| apply Rplus_le_reg_l with (thetat intr 0); unfold Rminus in |- *;
rewrite (Rplus_comm (thetat intr t));
repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_r;
rewrite Rplus_0_l; assumption ]
| apply Rplus_le_reg_l with (thetat intr 0); unfold Rminus in |- *;
rewrite (Rplus_comm (thetat intr t)); repeat rewrite <- Rplus_assoc;
rewrite Rplus_opp_r; rewrite Rplus_0_l; assumption ] ] ].
Qed.

Lemma xp0 : xp 0 = (- l × cos (thetat intr 0 + beta))%R.
unfold xp in |- *; rewrite xe_0; rewrite ye_0;
rewrite <- (Rplus_comm (xi intr 0)); unfold Rminus in |- *;
repeat rewrite Ropp_plus_distr; repeat rewrite <- Rplus_assoc;
repeat rewrite Rplus_opp_r; repeat rewrite Rplus_0_l;
rewrite cos_plus; ring.
Qed.

Definition hx (t : R) : R := (r_vi × sin (rho_vi × t))%R.

Lemma hx_derivable : derivable hx.
unfold hx in |- *; reg.
Qed.

Lemma Dhx :
t : R,
derive_pt hx t (hx_derivable t) = (vi intr × cos (rho_vi × t))%R.
Proof with trivial.
intro; unfold hx in |- *; reg...
replace (vi intr:R) with (r_vi × rho_vi)%R.
ring.
unfold rho_vi, r_vi in |- *; unfold r in |- ×.
field.
assert (H := rho_pos (vi intr)); red in |- *; intro; rewrite H0 in H;
elim (Rlt_irrefl _ H)...
Qed.

Lemma xpt :
t : R, (0 t)%R (rho_vi × t PI)%R (hx t xp t - xp 0)%R.
intros; replace (hx t) with (hx t - hx 0)%R.
apply (IAF_var xp hx 0 t xp_derivable hx_derivable H); intros; rewrite Dhx;
elim H1; intros;
apply
(Dx0_PI c H2 (Rle_trans (rho_vi × c) (rho_vi × t) PI (rho_t_le c t H3) H0)).
unfold hx in |- *; rewrite Rmult_0_r; rewrite sin_0; unfold Rminus in |- *;
rewrite Rmult_0_r; rewrite Ropp_0; apply Rplus_0_r.
Qed.

Lemma r_sin_pos :
t : R,
(0 t)%R (rho_vi × t PI)%R (0 r_vi × sin (rho_vi × t))%R.
intros; apply Rmult_le_pos;
[ left; unfold r_vi in |- *; unfold r in |- *; unfold Rdiv in |- *;
apply Rmult_lt_0_compat;
[ apply (TypeSpeed_pos (vi intr))
| apply Rinv_0_lt_compat; apply (rho_pos (vi intr)) ]
| apply sin_ge_0; [ apply (rho_t_pos t H) | assumption ] ].
Qed.

Lemma xpt_pos :
t : R, (0 t)%R (rho_vi × t PI)%R (0 xp t - xp 0)%R.
intros; generalize (xpt t H H0); unfold hx in |- *; intro;
apply Rle_trans with (r_vi × sin (rho_vi × t))%R;
[ apply (r_sin_pos t H H0) | assumption ].
Qed.

Lemma xpt_PI :
t : R,
(0 t)%R
(rho_vi × t PI)%R
(r_vi × sin (rho_vi × t) - l × cos (beta + thetat intr 0) xp t)%R.
intros; generalize (xpt t H H0); intro; unfold Rminus, hx in H1;
rewrite xp0 in H1;
generalize
(Rplus_le_compat_l (- l × cos (thetat intr 0 + beta))
(r_vi × sin (rho_vi × t)) (xp t + - (- l × cos (thetat intr 0 + beta)))
H1); rewrite <- (Rplus_comm (r_vi × sin (rho_vi × t)));
rewrite (Rplus_comm (- l × cos (thetat intr 0 + beta)));
repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
rewrite (Rplus_comm beta); unfold Rminus in |- *;
intro;
replace (- (l × cos (thetat intr 0 + beta)))%R with
(- l × cos (thetat intr 0 + beta))%R; [ assumption | ring ].
Qed.

Lemma Omega_defeq :
x : R, Omega x = true (PI / 2 x 3 × (PI / 2))%R.
Proof with trivial.
intro x; unfold Omega in |- ×...
case (Rle_dec (PI / 2) x); intro...
case (Rle_dec x (3 × (PI / 2))); intros...
split...
elim diff_false_true...
intro; elim diff_false_true...
Qed.

Lemma neg_cos_var : x : R, cos (x - PI) = (- cos x)%R.
intro; rewrite cos_minus; rewrite cos_PI; rewrite sin_PI; ring.
Qed.

Lemma xp0_pos : Omega (beta + thetat intr 0) = true (0 xp 0)%R.
Proof with trivial.
intro; generalize (Omega_defeq (beta + thetat intr 0) H); intro; rewrite xp0;
replace (- l × cos (thetat intr 0 + beta))%R with
(l × - cos (thetat intr 0 + beta))%R...
apply Rmult_le_pos...
apply l_is_pos...
rewrite <- neg_cos_var; unfold Rminus in |- *; elim H0; intros;
apply cos_ge_0...
apply Rplus_le_reg_l with PI; replace (PI + - (PI / 2))%R with (PI / 2)%R...
rewrite (Rplus_comm PI); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_r; rewrite <- (Rplus_comm beta)...
pattern PI at 2 in |- *; rewrite double_var; ring...
apply Rplus_le_reg_l with PI; replace (PI + PI / 2)%R with (3 × (PI / 2))%R...
rewrite (Rplus_comm PI); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_r; rewrite <- (Rplus_comm beta)...
pattern PI at 2 in |- *; rewrite double_var; ring...
ring...
Qed.

Lemma xpt_Omega :
t : R,
(0 t)%R
(rho_vi × t PI)%R
Omega (beta + thetat intr 0) = true (r_vi × sin (rho_vi × t) xp t)%R.
intros; generalize (xpt t H H0); intro; generalize (xp0_pos H1); intro;
unfold hx in H2;
generalize
(Rplus_le_compat_r (xp 0) (r_vi × sin (rho_vi × t)) (xp t - xp 0) H2);
unfold Rminus in |- *; repeat rewrite Rplus_assoc;
rewrite Rplus_opp_l; rewrite Rplus_0_r; intro;
apply (plus_le_is_le (r_vi × sin (rho_vi × t)) (xp 0) (xp t) H3 H4).
Qed.

t : R, Rsqr_evader_distance t = (Rsqr (xp t) + Rsqr (yp t))%R.
intro; unfold Rsqr_evader_distance, xp, yp in |- *; repeat rewrite Rsqr_plus;
ring_simplify; repeat rewrite Rsqr_mult;
rewrite <- (Rsqr_neg (sin (thetat intr 0)));
pattern (Rsqr (xi intr t - xe)) at 1 in |- ×.
replace (Rsqr (xi intr t - xe)) with
((Rsqr (sin (thetat intr 0)) + Rsqr (cos (thetat intr 0))) ×
Rsqr (xi intr t - xe))%R.
pattern (Rsqr (yi intr t - ye)) at 1 in |- ×.
replace (Rsqr (yi intr t - ye)) with
((Rsqr (sin (thetat intr 0)) + Rsqr (cos (thetat intr 0))) ×
Rsqr (yi intr t - ye))%R.
ring.
rewrite sin2_cos2 in |- *; ring.
rewrite sin2_cos2 in |- *; ring.
Qed.

Lemma xpt_xp0 :
t : R,
(xp t - xp 0)%R =
(cos (thetat intr 0) × (xi intr t - xi intr 0) +
sin (thetat intr 0) × (yi intr t - yi intr 0))%R.
intro; unfold xp in |- *; ring.
Qed.

Lemma ypt_yp0 :
t : R,
(yp t - yp 0)%R =
(- sin (thetat intr 0) × (xi intr t - xi intr 0) +
cos (thetat intr 0) × (yi intr t - yi intr 0))%R.
intro; unfold yp in |- *; ring.
Qed.

Lemma isometric_intruder :
t : R,
Rsqr_intruder_distance t = (Rsqr (xp t - xp 0) + Rsqr (yp t - yp 0))%R.
intro; unfold Rsqr_intruder_distance in |- *; rewrite xpt_xp0;
rewrite ypt_yp0; repeat rewrite Rsqr_plus; ring_simplify;
repeat rewrite Rsqr_mult;
rewrite <- Rsqr_neg.
pattern (Rsqr (xi intr t - xi intr 0)) at 1 in |- ×.
replace (Rsqr (xi intr t - xi intr 0)) with
((Rsqr (sin (thetat intr 0)) + Rsqr (cos (thetat intr 0))) ×
Rsqr (xi intr t - xi intr 0))%R.
pattern (Rsqr (yi intr t - yi intr 0)) at 1 in |- ×.
replace (Rsqr (yi intr t - yi intr 0)) with
((Rsqr (sin (thetat intr 0)) + Rsqr (cos (thetat intr 0))) ×
Rsqr (yi intr t - yi intr 0))%R.
ring.
rewrite sin2_cos2 in |- *; ring.
rewrite sin2_cos2 in |- *; ring.
Qed.

Lemma majoration :
t : R,
(Rsqr (yp t) Rsqr_evader_distance t)%R
(Rsqr (xp t) Rsqr_evader_distance t)%R.
intro; generalize (isometric_evader t); intro; split;
[ rewrite H; pattern (Rsqr (yp t)) at 1 in |- *;
rewrite <- (Rplus_0_l (Rsqr (yp t))); apply Rplus_le_compat_r;
apply Rle_0_sqr
| rewrite H; pattern (Rsqr (xp t)) at 1 in |- *;
rewrite <- (Rplus_0_r (Rsqr (xp t))); apply Rplus_le_compat_l;
apply Rle_0_sqr ].
Qed.

t : R, (0 t)%R (l - v (vi intr) × t e t)%R.
intros; cut (i t vi intr × t)%R;
[ intros; unfold Rminus in |- *; rewrite Rplus_comm;
apply Rplus_le_reg_l with (vi intr × t)%R; repeat rewrite <- Rplus_assoc;
rewrite Rplus_opp_r; rewrite Rplus_0_l; rewrite Rplus_comm;
apply Rle_trans with (e t + i t)%R;
[ apply L_intruder | apply Rplus_le_compat_l; assumption ]
| unfold i in |- *; unfold Rsqr_intruder_distance in |- *;
apply (YCNGFTYS intr t H) ].
Qed.

t : R,
(0 t)%R
(rho_vi × t < 2)%R (2 × r_vi × sin (rho_vi × (t / 2)) - l e t)%R.
intros; cut (2 × r_vi × sin (rho_vi × (t / 2)) i t)%R;
[ intro; intros; unfold Rminus in |- *; rewrite Rplus_comm;
apply Rplus_le_reg_l with l; repeat rewrite <- Rplus_assoc;
rewrite Rplus_opp_r; rewrite Rplus_0_l; apply Rle_trans with (i t);
[ assumption | apply L_i ]
| unfold i in |- *; unfold Rsqr_intruder_distance in |- *;
apply (YCNGSTYS intr t H H0) ].
Qed.

Lemma xp_pos :
t : R,
(0 t)%R
(rho_vi × t PI)%R Omega (beta + thetat intr 0) = true (0 xp t)%R.
intros; apply Rle_trans with (r_vi × sin (rho_vi × t))%R;
[ apply Rmult_le_pos;
[ unfold r_vi in |- *; unfold r in |- *; left; unfold Rdiv in |- *;
apply Rmult_lt_0_compat;
[ apply TypeSpeed_pos | apply Rinv_0_lt_compat; apply rho_pos ]
| apply sin_ge_0;
[ apply Rmult_le_pos;
[ unfold rho_vi in |- *; left; apply rho_pos | assumption ]
| assumption ] ]
| apply (xpt_Omega t H H0 H1) ].
Qed.

Lemma no_conflict_xp_1_Omega :
t : R,
(1 t)%R
(rho_vi × t PI - rho_vi)%R
Omega (beta + thetat intr 0) = true (ConflictRange < xp t)%R.
Proof with trivial.
intros; apply Rlt_le_trans with (r_vi × sin rho_vi)%R...
apply r_sin_rho...
apply Rle_trans with (r_vi × sin (rho_vi × t))%R...
apply Rmult_le_compat_l...
left; unfold r_vi in |- *; unfold r in |- *; unfold Rdiv in |- *;
apply Rmult_lt_0_compat...
apply TypeSpeed_pos...
apply Rinv_0_lt_compat; apply rho_pos...
case (Rle_dec (rho_vi × t) (PI / 2)); intro...
cut (rho_vi rho_vi × t)%R...
intro; apply sin_incr_1...
left; apply Rlt_trans with 0%R...
apply _PI2_RLT_0...
unfold rho_vi in |- *; apply rho_pos...
apply Rle_trans with (rho_vi × t)%R...
left; apply Rlt_le_trans with 0%R...
apply _PI2_RLT_0...
apply rho_t_pos...
left; apply Rlt_le_trans with 1%R; try apply Rlt_0_1...
pattern rho_vi at 1 in |- *; rewrite <- (Rmult_1_r rho_vi)...
apply Rmult_le_compat_l...
left; unfold rho_vi in |- *; apply rho_pos...
cut (PI / 2 < rho_vi × t)%R...
intro; cut (rho_vi PI - rho_vi × t)%R...
cut (PI - rho_vi × t PI / 2)%R...
intros; rewrite <- (sin_PI_x (rho_vi × t))...
apply sin_incr_1...
left; apply Rlt_trans with 0%R...
apply _PI2_RLT_0...
unfold rho_vi in |- *; apply rho_pos...
apply Rle_trans with (PI - rho_vi × t)%R...
apply Rle_trans with rho_vi...
left; apply Rlt_trans with 0%R...
apply _PI2_RLT_0...
unfold rho_vi in |- *; apply rho_pos...
left...
apply Rplus_lt_reg_r with (- (PI / 2) + rho_vi × t)%R...
replace (- (PI / 2) + rho_vi × t + (PI - rho_vi × t))%R with (PI / 2)%R...
replace (- (PI / 2) + rho_vi × t + PI / 2)%R with (rho_vi × t)%R...
ring...
unfold Rminus in |- *; unfold Rdiv in |- *;
replace (- (PI × / 2) + rho_vi × t + (PI + - (rho_vi × t)))%R with
(- (PI × / 2) + PI + (rho_vi × t + - (rho_vi × t)))%R...
rewrite Rplus_opp_r; rewrite Rplus_0_r...
pattern PI at 3 in |- *; rewrite double_var...
unfold Rdiv in |- *; ring...
ring...
apply Rplus_le_reg_l with (rho_vi × t - rho_vi)%R...
unfold Rminus in |- ×...
repeat rewrite Rplus_assoc...
rewrite Rplus_opp_l; rewrite Rplus_0_r...
rewrite (Rplus_comm (rho_vi × t))...
repeat rewrite Rplus_assoc...
rewrite Rplus_opp_l; rewrite Rplus_0_r...
rewrite <- (Rplus_comm PI)...
auto with real...
cut (0 t)%R...
cut (rho_vi × t PI)%R...
intros...
generalize (xpt t H3 H2); intro...
generalize (xp0_pos H1); intro...
unfold Rminus in H4...
generalize (Rplus_le_compat_r (xp 0) (hx t) (xp t + - xp 0) H4)...
repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r...
intro...
generalize (plus_le_is_le (hx t) (xp 0) (xp t) H5 H6)...
apply Rle_trans with (PI - rho_vi)%R...
apply Rplus_le_reg_l with (- PI)%R...
unfold Rminus in |- ×...
repeat rewrite <- Rplus_assoc...
repeat rewrite Rplus_opp_l...
rewrite Rplus_0_l...
rewrite <- Ropp_0...
apply Ropp_ge_le_contravar; apply Rle_ge; left; unfold rho_vi in |- *;
apply rho_pos...
left; apply Rlt_le_trans with 1%R; try apply Rlt_0_1...
Qed.

Lemma no_conflict_scenario_1_Omega :
t : R,
(1 t)%R
(rho_vi × t PI - rho_vi)%R
Omega (beta + thetat intr 0) = true
(Rsqr ConflictRange < Rsqr_evader_distance t)%R.
Proof with trivial.
intros; apply Rlt_le_trans with (Rsqr (xp t))...
apply Rsqr_incrst_1...
apply (no_conflict_xp_1_Omega t H H0 H1)...
unfold ConflictRange in |- *; left; prove_sup...
cut ((0 t)%R (rho_vi × t PI)%R)...
intro; elim H2; intros; apply (xp_pos t H3 H4 H1)...
split...
left; apply Rlt_le_trans with 1%R; try apply Rlt_0_1...
unfold Rminus in H0;
generalize (Rplus_le_compat_r rho_vi (rho_vi × t) (PI + - rho_vi) H0);
repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
intro; apply (plus_le_is_le (rho_vi × t) rho_vi PI)...
unfold rho_vi in |- *; left; apply rho_pos...
elim (majoration t)...
Qed.

Lemma no_conflict_scenario_0_1s :
t : R,
(0 t)%R
(t < 1)%R (ConflictRange + vi intr < l)%R (ConflictRange < e t)%R.
Proof with trivial.
intros; apply Rlt_le_trans with (l - vi intr × t)%R...
apply Rplus_lt_reg_r with (v (vi intr));
rewrite <- (Rplus_comm ConflictRange); apply Rlt_trans with l...
apply Rplus_lt_reg_r with (- l)%R; rewrite Rplus_opp_l;
replace (- l + (vi intr + (l - vi intr × t)))%R with (vi intr × (1 - t))%R...
apply Rmult_lt_0_compat...
apply TypeSpeed_pos...
generalize (Rplus_lt_compat_r (- t) t 1 H0); rewrite Rplus_opp_r...
unfold Rminus in |- *; rewrite Rmult_plus_distr_l; ring...
apply (YCNGFTYS_evader t H)...
Qed.

Lemma no_conflict_gt_max_t :
t : R,
let MaxDistance := (vi intr × t + ConflictRange)%R in
(0 t)%R (MaxDistance < l)%R (ConflictRange < e t)%R.
Proof with trivial.
intros; apply Rlt_le_trans with (l - vi intr × t)%R...
unfold MaxDistance in H0; rewrite Rplus_comm in H0;
generalize
(Rplus_lt_compat_r (- (vi intr × t)) (ConflictRange + vi intr × t) l H0);
repeat rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r...
apply (YCNGFTYS_evader t H)...
Qed.

Lemma no_conflict_lt_min_t :
t : R,
let MinDistance := (2 × r_vi × sin (rho_vi × (t / 2)) - ConflictRange)%R in
(0 t)%R
(0 rho_vi × t)%R
(rho_vi × t < 2)%R (l < MinDistance)%R (ConflictRange < e t)%R.
Proof with trivial.
intros; apply Rlt_le_trans with (2 × r_vi × sin (rho_vi × (t / 2)) - l)%R...
unfold MinDistance in H2; apply Rplus_lt_reg_r with (- ConflictRange + l)%R;
replace (- ConflictRange + l + ConflictRange)%R with l...
replace (- ConflictRange + l + (2 × r_vi × sin (rho_vi × (t / 2)) - l))%R
with (2 × r_vi × sin (rho_vi × (t / 2)) - ConflictRange)%R;
try ring...
ring...
apply (YCNGSTYS_evader t H H1)...
Qed.

Lemma no_conflict_Omega_t :
t : R,
(ConflictRange + vi intr < l)%R
(0 t)%R
(rho_vi × t PI - rho_vi)%R
Omega (beta + thetat intr 0) = true (ConflictRange < e t)%R.
intros; case (Rle_dec 1 t); intro.
apply Rsqr_incrst_0.
unfold e in |- *; rewrite Rsqr_sqrt.
apply (no_conflict_scenario_1_Omega t r H1 H2).
left; unfold ConflictRange in |- *; prove_sup.
unfold e in |- *; apply sqrt_positivity; apply Rsqr_evader_distance_pos.
cut (t < 1)%R.
intro; apply (no_conflict_scenario_0_1s t H0 H3 H).
auto with real.
Qed.

Theorem no_conflict_gt_max :
let MaxDistance := (vi intr × T + ConflictRange)%R in
(MaxDistance < l)%R conflict T = false.
Proof with trivial.
intros; unfold conflict in |- *; case (Rle_dec (Die T T) ConflictRange);
intro...
cut (0 T)%R...
intro; generalize (no_conflict_gt_max_t T H0 H); intro; cut (e T = Die T T)...
intro; rewrite H2 in H1;
elim
(Rlt_irrefl (Die T T) (Rle_lt_trans (Die T T) ConflictRange (Die T T) r H1))...
left; apply Rlt_le_trans with MinT...
apply MinT_is_pos...
apply (cond_1 T)...
Qed.

Theorem no_conflict_lt_min :
let MinDistance := (2 × r_vi × sin (rho_vi × (T / 2)) - ConflictRange)%R in
(0 rho_vi × T)%R
(rho_vi × T < 2)%R (l < MinDistance)%R conflict T = false.
Proof with trivial.
intros; unfold conflict in |- *; case (Rle_dec (Die T T) ConflictRange);
intro...
cut (0 T)%R...
intro; generalize (no_conflict_lt_min_t T H2 H H0 H1); intro;
cut (e T = Die T T)...
intro; rewrite H4 in H3;
elim
(Rlt_irrefl (Die T T) (Rle_lt_trans (Die T T) ConflictRange (Die T T) r H3))...
left; apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ]...
Qed.

Theorem no_conflict_Omega :
(ConflictRange + v (vi intr) < l)%R
(rho_vi × T PI - rho_vi)%R
Omega (beta + thetat intr 0) = true conflict T = false.
Proof with trivial.
intros; unfold conflict in |- *; case (Rle_dec (Die T T) ConflictRange);
intro...
cut (0 T)%R...
intro; generalize (no_conflict_Omega_t T H H2 H0 H1); intro;
cut (e T = Die T T)...
intro; rewrite H4 in H3;
elim
(Rlt_irrefl (Die T T) (Rle_lt_trans (Die T T) ConflictRange (Die T T) r H3))...
left; apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ]...
Qed.

End trajectory.