(* 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                                                     *)


Require Import Reals.
Require Import trajectory_const.
Require Import rrho.
Require Import constants.
Require Import Omega.

(* Verifiable in MuPAD *)
Axiom
  Math_prop_alarm_1 :
    forall (a l : R) (T : TimeT),
    (MinDistance T <= l)%R ->
    (l <= MaxDistance T)%R ->
    (0 <= a)%R ->
    (a <= MinBeta)%R ->
    (Rsqr (l * cos a - v V * T) + Rsqr (l * sin a) <= Rsqr AlertRange)%R.

(* Verifiable in MuPAD *)
Axiom
  Math_prop_no_conflict_1 :
    forall (a l x y : R) (T : TimeT),
    (MinDistance T <= l)%R ->
    (l <= MaxDistance T)%R ->
    (MinBeta <= a)%R ->
    (a <= PI / 2)%R ->
    (l * sin a + r_V * (cos (rho_V * T) - 1) <= y)%R ->
    (r_V * sin (rho_V * T) - l * cos a <= x)%R ->
    (Rsqr ConflictRange < Rsqr x + Rsqr y)%R.

(**********)
Lemma MinBeta_pos : (0 < MinBeta)%R.
(* Goal: Rlt (IZR Z0) MinBeta *)
unfold MinBeta in |- *; unfold Rdiv in |- *.
(* Goal: Rlt (IZR Z0) (Rmult (IZR (Zpos (xI (xI (xO (xI (xI (xO (xO (xO (xO xH))))))))))) (Rinv (IZR (Zpos (xO (xO (xO (xI (xO (xI (xI (xI (xI xH))))))))))))) *)
apply Rmult_lt_0_compat; [ prove_sup | apply Rinv_0_lt_compat; prove_sup ].
Qed.

(**********)
Lemma Math_prop_y_a_PI2 :
 forall (a l : R) (T : TimeT),
 (MinBeta <= a)%R ->
 (a <= PI / 2)%R ->
 (0 <= l)%R ->
 (l * sin MinBeta + r_V * (cos (rho_V * T) - 1) <=
  l * sin a + r_V * (cos (rho_V * T) - 1))%R. 
intros; apply Rplus_le_compat_r; apply Rmult_le_compat_l;
 [ assumption
 | apply sin_incr_1;
    [ left; apply Rlt_trans with 0%R;
       [ apply _PI2_RLT_0 | apply MinBeta_pos ]
    | apply Rle_trans with a; assumption
    | left; apply Rlt_trans with 0%R;
       [ apply _PI2_RLT_0
       | apply Rlt_le_trans with MinBeta; [ apply MinBeta_pos | assumption ] ]
    | assumption
    | assumption ] ].
Qed.

(**********)
Lemma Math_prop_approx_y_a_PI2 :
 forall (a l1 l2 : R) (T : TimeT),
 (0 <= a)%R ->
 (a <= PI / 2)%R ->
 (0 <= l1)%R ->
 (l1 <= l2)%R ->
 (l1 * sin_lb a + r_ub V * (cos_lb (rho_ub V * MaxT) - 1) <=
  l2 * sin a + r_V * (cos (rho_V * T) - 1))%R.
(* Goal: forall (a l1 l2 : R) (T : TimeT) (_ : Rle (IZR Z0) a) (_ : Rle a (Rdiv PI (IZR (Zpos (xO xH))))) (_ : Rle (IZR Z0) l1) (_ : Rle l1 l2), Rle (Rplus (Rmult l1 (sin_lb a)) (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) (Rplus (Rmult l2 (sin a)) (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
intros; apply Rplus_le_compat.
(* Goal: Rle (Rmult l1 (sin_lb a)) (Rmult l2 (sin a)) *)
(* Goal: Rle (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH)))) (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH)))) *)
apply Rle_trans with (l1 * sin a)%R.
(* Goal: Rle (Rmult l1 (sin_lb a)) (Rmult l1 (sin a)) *)
(* Goal: Rle (Rmult l1 (sin a)) (Rmult l2 (sin a)) *)
(* Goal: Rle (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH)))) (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH)))) *)
apply Rmult_le_compat_l.
(* Goal: Rle (IZR Z0) a *)
assumption.
generalize (SIN a H (Rlt_le a PI (Rle_lt_trans a (PI / 2) PI H0 PI2_Rlt_PI)));
(* Goal: Rle (IZR Z0) a *)
 intro; elim H3; intros; assumption.
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V MinT) *)
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (sin a) *)
(* Goal: Rle l1 l2 *)
(* Goal: Rle (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH)))) (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH)))) *)
apply (sin_ge_0 a H (Rlt_le a PI (Rle_lt_trans a (PI / 2) PI H0 PI2_Rlt_PI))).
(* Goal: Rle (IZR Z0) a *)
assumption.
rewrite <- (Ropp_involutive (r_ub V * (cos_lb (rho_ub V * MaxT) - 1)));
 rewrite <- (Ropp_involutive (r_V * (cos (rho_V * T) - 1)));
 apply Ropp_ge_le_contravar; apply Rle_ge;
 replace (- (r_V * (cos (rho_V * T) - 1)))%R with
  (r_V * (1 - cos (rho_V * T)))%R.
replace (- (r_ub V * (cos_lb (rho_ub V * MaxT) - 1)))%R with
 (r_ub V * (1 - cos_lb (rho_ub V * MaxT)))%R.
(* Goal: Rle (Rmult l1 (cos a)) (Rmult l2 (cos_ub a)) *)
apply Rmult_le_compat.
(* Goal: Rle (IZR Z0) r_V *)
(* Goal: Rle (IZR Z0) (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T)))) *)
(* Goal: Rle r_V (r_ub V) *)
(* Goal: Rle (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T)))) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
left; apply r_V_is_pos.
apply Rplus_le_reg_l with (cos (rho_V * T)); rewrite Rplus_0_r;
 rewrite Rplus_comm; unfold Rminus in |- *; repeat rewrite Rplus_assoc;
 rewrite Rplus_opp_l; rewrite Rplus_0_r; generalize (COS_bound (rho_V * T));
(* Goal: Rle (IZR Z0) a *)
 intro; elim H3; intros; assumption.
(* Goal: Rle r_V (r_ub V) *)
(* Goal: Rle (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T)))) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
unfold r_V in |- *; left; apply r_ub_0.
apply Rplus_le_reg_l with (Ropp 1); unfold Rminus in |- *;
 repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l;
 repeat rewrite Rplus_0_l; apply Ropp_ge_le_contravar; 
 apply Rle_ge; apply Rle_trans with (cos (rho_ub V * MaxT)).
(* Goal: Rle (cos_lb (Rmult (rho_ub V) MaxT)) (cos (Rmult (rho_ub V) MaxT)) *)
(* Goal: Rle (cos (Rmult (rho_ub V) MaxT)) (cos (Rmult rho_V (val T))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
cut (- PI / 2 <= rho_ub V * MaxT <= PI / 2)%R.
intro; elim H3; intros; generalize (COS (rho_ub V * MaxT) H4 H5); intro;
(* Goal: Rle (IZR Z0) a *)
 elim H6; intros; assumption.
(* Goal: and (Rle (IZR Z0) (Rmult (rho_lb V) MinT)) (Rle (Rmult (rho_lb V) MinT) PI) *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
split.
(* Goal: Rle (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) a *)
left; apply Rlt_le_trans with 0%R.
(* Goal: Rlt (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) (IZR Z0) *)
(* Goal: Rle (IZR Z0) a *)
replace (- PI / 2)%R with (- (PI / 2))%R.
(* Goal: Rlt (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (IZR Z0) *)
(* Goal: @eq R (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (IZR Z0) a *)
apply _PI2_RLT_0.
unfold Rdiv in |- *; symmetry  in |- *; apply Ropp_mult_distr_l_reverse.
(* Goal: Rle (IZR Z0) (Rmult (rho_ub V) MaxT) *)
(* Goal: Rle (Rmult (rho_ub V) MaxT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (cos (Rmult (rho_ub V) MaxT)) (cos (Rmult rho_V (val T))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
apply Rmult_le_pos.
(* Goal: Rle (IZR Z0) (rho_ub V) *)
(* Goal: Rle (IZR Z0) MaxT *)
(* Goal: Rle (Rmult (rho_ub V) MaxT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (cos (Rmult (rho_ub V) MaxT)) (cos (Rmult rho_V (val T))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
left; apply rho_ub_pos.
(* Goal: Rle (IZR Z0) MaxT *)
(* Goal: Rle (Rmult (rho_ub V) MaxT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (cos (Rmult (rho_ub V) MaxT)) (cos (Rmult rho_V (val T))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
left; unfold MaxT in |- *.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rle (Rmult (rho_ub V) MaxT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (cos (Rmult (rho_ub V) MaxT)) (cos (Rmult rho_V (val T))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
prove_sup.
(* Goal: Rlt (Rmult (rho_ub V) MaxT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rdiv PI (IZR (Zpos (xO xH)))) PI *)
(* Goal: Rle (Rmult rho_V (val T)) (Rmult (rho_ub V) MaxT) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
cut (MaxT <= MaxT)%R.
(* Goal: forall _ : Rle MaxT MaxT, Rle (Rmult (rho_ub V) MaxT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle MaxT MaxT *)
(* Goal: Rle (cos (Rmult (rho_ub V) MaxT)) (cos (Rmult rho_V (val T))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
intro; left; apply (rho_ub_t_PI2 V (mkTimeT MaxT MinT_MaxT H3)).
(* Goal: Rle MinT MinT *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
right; reflexivity.
(* Goal: Rle (cos (Rmult (rho_ub V) MaxT)) (cos (Rmult rho_V (val T))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
apply cos_decr_1.
(* Goal: Rle (IZR Z0) (Rmult (rho_lb V) MinT) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) PI *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) rho_V *)
(* Goal: Rlt (IZR Z0) (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply rho_V_is_pos.
(* Goal: Rlt (IZR Z0) (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rlt_le_trans with MinT.
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply MinT_is_pos.
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply (cond_1 T).
(* Goal: Rle (Rmult (rho_ub V) MaxT) PI *)
(* Goal: Rle (Rmult rho_V (val T)) (Rmult (rho_ub V) MaxT) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
left; apply Rlt_trans with (PI / 2)%R.
(* Goal: Rlt (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rdiv PI (IZR (Zpos (xO xH)))) PI *)
(* Goal: Rle (IZR Z0) (Rmult (rho_ub V) MaxT) *)
(* Goal: Rle (Rmult (rho_ub V) MaxT) PI *)
(* Goal: Rle (Rmult rho_V (val T)) (Rmult (rho_ub V) MaxT) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
apply (rho_t_PI2 T). 
(* Goal: Rlt (Rdiv PI (IZR (Zpos (xO xH)))) PI *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply PI2_Rlt_PI.
(* Goal: Rle (IZR Z0) (Rmult (rho_lb V) MinT) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) PI *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) (rho_ub V) *)
(* Goal: Rlt (IZR Z0) MaxT *)
(* Goal: Rle (Rmult (rho_ub V) MaxT) PI *)
(* Goal: Rle (Rmult rho_V (val T)) (Rmult (rho_ub V) MaxT) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
apply rho_ub_pos.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO (xI (xO xH))))) *)
(* Goal: Rle (Rmult (rho_ub V) MaxT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (cos (Rmult (rho_ub V) MaxT)) (cos (Rmult rho_V (val T))) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
unfold MaxT in |- *; prove_sup.
(* Goal: Rle (Rmult (rho_ub V) MaxT) PI *)
(* Goal: Rle (Rmult rho_V (val T)) (Rmult (rho_ub V) MaxT) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
left; apply Rlt_trans with (PI / 2)%R.
(* Goal: Rlt (Rmult (rho_ub V) MaxT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rdiv PI (IZR (Zpos (xO xH)))) PI *)
(* Goal: Rle (Rmult rho_V (val T)) (Rmult (rho_ub V) MaxT) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
cut (MaxT <= MaxT)%R.
(* Goal: forall _ : Rle MaxT MaxT, Rlt (Rmult (rho_ub V) MaxT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle MaxT MaxT *)
(* Goal: Rlt (Rdiv PI (IZR (Zpos (xO xH)))) PI *)
(* Goal: Rle (Rmult rho_V (val T)) (Rmult (rho_ub V) MaxT) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
intro; apply (rho_ub_t_PI2 V (mkTimeT MaxT MinT_MaxT H3)).
(* Goal: Rle MinT MinT *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
right; reflexivity.
(* Goal: Rlt (Rdiv PI (IZR (Zpos (xO xH)))) PI *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply PI2_Rlt_PI.
(* Goal: Rle (Rmult l1 (cos a)) (Rmult l2 (cos_ub a)) *)
apply Rmult_le_compat.
(* Goal: Rlt (IZR Z0) rho_V *)
(* Goal: Rlt (IZR Z0) (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply rho_V_is_pos.
(* Goal: Rle (IZR Z0) (val T) *)
(* Goal: Rle rho_V (rho_ub V) *)
(* Goal: Rle (val T) MaxT *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
left; apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ].
(* Goal: Rle rho_V (rho_ub V) *)
(* Goal: Rle (val T) MaxT *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
left; unfold rho_V in |- *; apply rho_ub_0.
(* Goal: Rle (val T) MaxT *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
apply (cond_2 T).
(* Goal: @eq R (Rminus (Rplus (Rplus (Rdiv PI (IZR (Zpos (xO xH)))) (Rdiv PI (IZR (Zpos (xO xH))))) (Rplus (Rdiv PI (IZR (Zpos (xO xH)))) (Rdiv PI (IZR (Zpos (xO xH)))))) a) (Rplus (Rminus (Rdiv PI (IZR (Zpos (xO xH)))) a) (Rmult (IZR (Zpos (xI xH))) (Rdiv PI (IZR (Zpos (xO xH)))))) *)
(* Goal: Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
ring.
(* Goal: @eq R (Rminus (Rplus (Rplus (Rdiv PI (IZR (Zpos (xO xH)))) (Rdiv PI (IZR (Zpos (xO xH))))) (Rplus (Rdiv PI (IZR (Zpos (xO xH)))) (Rdiv PI (IZR (Zpos (xO xH)))))) a) (Rplus (Rminus (Rdiv PI (IZR (Zpos (xO xH)))) a) (Rmult (IZR (Zpos (xI xH))) (Rdiv PI (IZR (Zpos (xO xH)))))) *)
(* Goal: Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
ring.
Qed.

(**********)
Lemma Math_prop_x_a_PI2 :
 forall (a l : R) (T : TimeT),
 (MinBeta <= a)%R ->
 (a <= PI / 2)%R ->
 (0 <= l)%R ->
 (r_V * sin (rho_V * T) - l * cos MinBeta <=
  r_V * sin (rho_V * T) - l * cos a)%R.
intros; unfold Rminus in |- *; apply Rplus_le_compat_l;
 apply Ropp_ge_le_contravar; apply Rle_ge; apply Rmult_le_compat_l;
 [ assumption
 | apply cos_decr_1;
    [ left; apply MinBeta_pos
    | apply Rle_trans with a;
       [ assumption
       | left; apply Rle_lt_trans with (PI / 2)%R;
          [ assumption | apply PI2_Rlt_PI ] ]
    | left; apply Rlt_le_trans with MinBeta;
       [ apply MinBeta_pos | assumption ]
    | left; apply Rle_lt_trans with (PI / 2)%R;
       [ assumption | apply PI2_Rlt_PI ]
    | assumption ] ].
Qed.

(**********)
Lemma Math_prop_approx_x_a_PI2 :
 forall (a l1 l2 : R) (T : TimeT),
 (0 <= a)%R ->
 (a <= PI / 2)%R ->
 (0 <= l1)%R ->
 (l1 <= l2)%R ->
 (r_lb V * sin_lb (rho_lb V * MinT) - l2 * cos_ub a <=
  r_V * sin (rho_V * T) - l1 * cos a)%R.
(* Goal: forall (a l1 l2 : R) (T : TimeT) (_ : Rle (IZR Z0) a) (_ : Rle a (Rdiv PI (IZR (Zpos (xO xH))))) (_ : Rle (IZR Z0) l1) (_ : Rle l1 l2), Rle (Rminus (Rmult (r_lb V) (sin_lb (Rmult (rho_lb V) MinT))) (Rmult l2 (cos_ub a))) (Rminus (Rmult r_V (sin (Rmult rho_V (val T)))) (Rmult l1 (cos a))) *)
intros; unfold Rminus in |- *; apply Rplus_le_compat.
(* Goal: Rle (Rmult l1 (cos a)) (Rmult l2 (cos_ub a)) *)
apply Rmult_le_compat.
left; unfold r_lb in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat;
 [ apply TypeSpeed_pos | apply Rinv_0_lt_compat; apply rho_ub_pos ].
(* Goal: Rle (IZR Z0) (sin_lb (Rmult (rho_lb V) MinT)) *)
(* Goal: Rle (r_lb V) r_V *)
(* Goal: Rle (sin_lb (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply sin_lb_ge_0.
(* Goal: Rle (IZR Z0) (Rmult (rho_lb V) MinT) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (r_lb V) r_V *)
(* Goal: Rle (sin_lb (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply Rmult_lt_0_compat; [ apply rho_lb_pos | apply MinT_is_pos ].
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rle_trans with (rho_V * MinT)%R.
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V MinT) *)
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rmult_le_compat_r.
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply MinT_is_pos.
(* Goal: Rle (rho_lb V) rho_V *)
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
unfold rho_V in |- *; left; apply rho_lb_0.
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
cut (MinT <= MinT)%R.
(* Goal: forall _ : Rle MinT MinT, Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle MinT MinT *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
intro; left; apply (rho_t_PI2 (mkTimeT MinT H3 MinT_MaxT)).
(* Goal: Rle MinT MinT *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
right; reflexivity.
(* Goal: Rle (r_lb V) r_V *)
(* Goal: Rle (sin_lb (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
unfold r_V in |- *; left; apply r_lb_0.
(* Goal: Rle (sin_lb (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rle_trans with (sin (rho_lb V * MinT)).
(* Goal: Rle (sin_lb (Rmult (rho_lb V) MinT)) (sin (Rmult (rho_lb V) MinT)) *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
cut (0 <= rho_lb V * MinT <= PI)%R.
(* Goal: forall _ : and (Rle (IZR Z0) (Rmult (rho_lb V) MinT)) (Rle (Rmult (rho_lb V) MinT) PI), Rle (sin_lb (Rmult (rho_lb V) MinT)) (sin (Rmult (rho_lb V) MinT)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (rho_lb V) MinT)) (Rle (Rmult (rho_lb V) MinT) PI) *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
intro; elim H3; intros.
(* Goal: Rle (IZR Z0) a *)
generalize (SIN (rho_lb V * MinT) H4 H5); intro; elim H6; intros; assumption.
(* Goal: and (Rle (IZR Z0) (Rmult (rho_lb V) MinT)) (Rle (Rmult (rho_lb V) MinT) PI) *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
split.
(* Goal: Rle (IZR Z0) (Rmult (rho_lb V) MinT) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) PI *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) (rho_lb V) *)
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply rho_lb_pos.
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply MinT_is_pos.
(* Goal: Rle (Rmult (rho_lb V) MinT) PI *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply Rle_lt_trans with (PI / 2)%R.
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rle_trans with (rho_V * MinT)%R.
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V MinT) *)
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rmult_le_compat_r.
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply MinT_is_pos.
(* Goal: Rle (rho_lb V) rho_V *)
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
unfold rho_V in |- *; left; apply rho_lb_0.
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
cut (MinT <= MinT)%R.
(* Goal: forall _ : Rle MinT MinT, Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle MinT MinT *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
intro; left; apply (rho_t_PI2 (mkTimeT MinT H3 MinT_MaxT)).
(* Goal: Rle MinT MinT *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
right; reflexivity.
(* Goal: Rlt (Rdiv PI (IZR (Zpos (xO xH)))) PI *)
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply PI2_Rlt_PI.
(* Goal: Rle (sin (Rmult (rho_lb V) MinT)) (sin (Rmult rho_V (val T))) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply sin_incr_1.
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply Rlt_trans with 0%R.
(* Goal: Rlt (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (IZR Z0) *)
(* Goal: @eq R (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (IZR Z0) a *)
apply _PI2_RLT_0.
(* Goal: Rlt (IZR Z0) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) (rho_lb V) *)
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply rho_lb_pos.
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply MinT_is_pos.
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rle_trans with (rho_V * MinT)%R.
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V MinT) *)
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rmult_le_compat_r.
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply MinT_is_pos.
(* Goal: Rle (rho_lb V) rho_V *)
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
unfold rho_V in |- *; left; apply rho_lb_0.
(* Goal: Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
cut (MinT <= MinT)%R.
(* Goal: forall _ : Rle MinT MinT, Rle (Rmult rho_V MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle MinT MinT *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
intro; left; apply (rho_t_PI2 (mkTimeT MinT H3 MinT_MaxT)).
(* Goal: Rle MinT MinT *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
right; reflexivity.
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply Rlt_trans with 0%R.
(* Goal: Rlt (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (IZR Z0) *)
(* Goal: @eq R (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (IZR Z0) a *)
apply _PI2_RLT_0.
(* Goal: Rlt (IZR Z0) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) rho_V *)
(* Goal: Rlt (IZR Z0) (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply rho_V_is_pos.
(* Goal: Rlt (IZR Z0) (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Rlt_le_trans with MinT.
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply MinT_is_pos.
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply (cond_1 T).
(* Goal: Rlt (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rlt (Rdiv PI (IZR (Zpos (xO xH)))) PI *)
(* Goal: Rle (IZR Z0) (Rmult (rho_ub V) MaxT) *)
(* Goal: Rle (Rmult (rho_ub V) MaxT) PI *)
(* Goal: Rle (Rmult rho_V (val T)) (Rmult (rho_ub V) MaxT) *)
(* Goal: @eq R (Rmult (r_ub V) (Rminus (IZR (Zpos xH)) (cos_lb (Rmult (rho_ub V) MaxT)))) (Ropp (Rmult (r_ub V) (Rminus (cos_lb (Rmult (rho_ub V) MaxT)) (IZR (Zpos xH))))) *)
(* Goal: @eq R (Rmult r_V (Rminus (IZR (Zpos xH)) (cos (Rmult rho_V (val T))))) (Ropp (Rmult r_V (Rminus (cos (Rmult rho_V (val T))) (IZR (Zpos xH))))) *)
left; apply (rho_t_PI2 T).
(* Goal: Rle (Rmult l1 (cos a)) (Rmult l2 (cos_ub a)) *)
apply Rmult_le_compat.
(* Goal: Rlt (IZR Z0) (rho_lb V) *)
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rmult rho_V (val T)) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply rho_lb_pos.
(* Goal: Rlt (IZR Z0) MinT *)
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Rmult rho_V (val T)) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (Rmult (rho_lb V) MinT) (Rmult rho_V (val T)) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; apply MinT_is_pos.
(* Goal: Rle (rho_lb V) rho_V *)
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
left; unfold rho_V in |- *; apply rho_lb_0.
(* Goal: Rle MinT (val T) *)
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply (cond_1 T).
(* Goal: Rle (Ropp (Rmult l2 (cos_ub a))) (Ropp (Rmult l1 (cos a))) *)
apply Ropp_ge_le_contravar; apply Rle_ge.
(* Goal: Rle (Rmult l1 (cos a)) (Rmult l2 (cos_ub a)) *)
apply Rmult_le_compat.
(* Goal: Rle (IZR Z0) a *)
assumption.
(* Goal: Rle (IZR Z0) (cos a) *)
(* Goal: Rle l1 l2 *)
(* Goal: Rle (cos a) (cos_ub a) *)
apply cos_ge_0.
(* Goal: Rle (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) a *)
left; apply Rlt_le_trans with 0%R.
(* Goal: Rlt (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (IZR Z0) *)
(* Goal: @eq R (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (IZR Z0) a *)
apply _PI2_RLT_0.
(* Goal: Rle (IZR Z0) a *)
assumption.
(* Goal: Rle (IZR Z0) a *)
assumption.
(* Goal: Rle (IZR Z0) a *)
assumption.
(* Goal: Rle (cos a) (cos_ub a) *)
cut (- PI / 2 <= a)%R.
(* Goal: Rle (IZR Z0) a *)
intro; generalize (COS a H3 H0); intro; elim H4; intros; assumption.
(* Goal: Rle (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) a *)
left; apply Rlt_le_trans with 0%R.
(* Goal: Rlt (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) (IZR Z0) *)
(* Goal: Rle (IZR Z0) a *)
replace (- PI / 2)%R with (- (PI / 2))%R.
(* Goal: Rlt (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (IZR Z0) *)
(* Goal: @eq R (Ropp (Rdiv PI (IZR (Zpos (xO xH))))) (Rdiv (Ropp PI) (IZR (Zpos (xO xH)))) *)
(* Goal: Rle (IZR Z0) a *)
apply _PI2_RLT_0.
unfold Rdiv in |- *; symmetry  in |- *; apply Ropp_mult_distr_l_reverse.
(* Goal: Rle (IZR Z0) a *)
assumption.
Qed.

(**********)
Lemma Math_prop_no_conflict_2 :
 forall (a l x y : R) (T : TimeT),
 (MinDistance T <= l)%R ->
 (l <= MaxDistance T)%R ->
 (3 * (PI / 2) <= a)%R ->
 (a <= 2 * PI - MinBeta)%R ->
 (y <= l * sin a - r_V * (cos (rho_V * T) - 1))%R ->
 (r_V * sin (rho_V * T) - l * cos a <= x)%R ->
 (Rsqr ConflictRange < Rsqr x + Rsqr y)%R.
(* Goal: forall (a l : R) (T : TimeT) (_ : Rle (MinDistance T) l) (_ : Rle l (MaxDistance T)) (_ : Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) MinBeta) a) (_ : Rle a (Rmult (IZR (Zpos (xO xH))) PI)), Rle (Rplus (Rsqr (Rminus (Rmult l (cos a)) (Rmult (v V) (val T)))) (Rsqr (Rmult l (sin a)))) (Rsqr AlertRange) *)
intros.
(* Goal: Rlt (Rsqr ConflictRange) (Rplus (Rsqr x) (Rsqr y)) *)
cut (MinBeta <= 2 * PI - a)%R.
(* Goal: forall _ : Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a), Rlt (Rsqr ConflictRange) (Rplus (Rsqr x) (Rsqr y)) *)
(* Goal: Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
cut (2 * PI - a <= PI / 2)%R.
(* Goal: forall (_ : Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) (Rdiv PI (IZR (Zpos (xO xH))))) (_ : Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a)), Rlt (Rsqr ConflictRange) (Rplus (Rsqr x) (Rsqr y)) *)
(* Goal: Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
cut (l * sin (2 * PI - a) + r_V * (cos (rho_V * T) - 1) <= - y)%R.
intros; rewrite (Rsqr_neg y);
 apply (Math_prop_no_conflict_1 (2 * PI - a) l x (- y) T H H0 H7 H6 H5).
replace (2 * PI - a)%R with (- a + 2 * INR 1 * PI)%R;
 [ rewrite (cos_period (- a) 1); rewrite cos_neg; assumption | simpl; ring ].
replace (2 * PI - a)%R with (- a + 2 * INR 1 * PI)%R;
 [ rewrite (sin_period (- a) 1); rewrite sin_neg;
    replace (l * - sin a + r_V * (cos (rho_V * T) - 1))%R with
     (- (l * sin a - r_V * (cos (rho_V * T) - 1)))%R;
    [ apply Ropp_ge_le_contravar; apply Rle_ge; assumption | simpl; ring ]
 | simpl; ring ].
generalize (Rplus_le_compat_l (PI / 2 - a) (3 * (PI / 2)) a H1);
 replace (PI / 2 - a + 3 * (PI / 2))%R with (2 * PI - a)%R.
(* Goal: forall _ : Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) (Rplus (Rminus (Rdiv PI (IZR (Zpos (xO xH)))) a) a), Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) (Rdiv PI (IZR (Zpos (xO xH)))) *)
(* Goal: @eq R (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) (Rplus (Rminus (Rdiv PI (IZR (Zpos (xO xH)))) a) (Rmult (IZR (Zpos (xI xH))) (Rdiv PI (IZR (Zpos (xO xH)))))) *)
(* Goal: Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
replace (PI / 2 - a + a)%R with (PI / 2)%R.
(* Goal: Rle (IZR Z0) a *)
intro; assumption.
unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_l;
 rewrite Rplus_0_r; reflexivity. 
(* Goal: @eq R (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) (Rplus (Rminus (Rdiv PI (IZR (Zpos (xO xH)))) a) (Rmult (IZR (Zpos (xI xH))) (Rdiv PI (IZR (Zpos (xO xH)))))) *)
(* Goal: Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
rewrite double.
(* Goal: @eq R (Rminus (Rplus PI PI) a) (Rplus (Rminus (Rdiv PI (IZR (Zpos (xO xH)))) a) (Rmult (IZR (Zpos (xI xH))) (Rdiv PI (IZR (Zpos (xO xH)))))) *)
(* Goal: Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
pattern PI at 1 2 in |- *; rewrite double_var.
(* Goal: @eq R (Rminus (Rplus (Rplus (Rdiv PI (IZR (Zpos (xO xH)))) (Rdiv PI (IZR (Zpos (xO xH))))) (Rplus (Rdiv PI (IZR (Zpos (xO xH)))) (Rdiv PI (IZR (Zpos (xO xH)))))) a) (Rplus (Rminus (Rdiv PI (IZR (Zpos (xO xH)))) a) (Rmult (IZR (Zpos (xI xH))) (Rdiv PI (IZR (Zpos (xO xH)))))) *)
(* Goal: Rle MinBeta (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
ring.
generalize (Rplus_le_compat_l (MinBeta - a) a (2 * PI - MinBeta) H2);
 replace (MinBeta - a + (2 * PI - MinBeta))%R with (2 * PI - a)%R;
 [ replace (MinBeta - a + a)%R with MinBeta; [ intro; assumption | ring ]
 | ring ].
Qed.

(**********)
Lemma Math_prop_alarm_2 :
 forall (a l : R) (T : TimeT),
 (MinDistance T <= l)%R ->
 (l <= MaxDistance T)%R ->
 (2 * PI - MinBeta <= a)%R ->
 (a <= 2 * PI)%R ->
 (Rsqr (l * cos a - v V * T) + Rsqr (l * sin a) <= Rsqr AlertRange)%R.
(* Goal: forall (a l : R) (T : TimeT) (_ : Rle (MinDistance T) l) (_ : Rle l (MaxDistance T)) (_ : Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) MinBeta) a) (_ : Rle a (Rmult (IZR (Zpos (xO xH))) PI)), Rle (Rplus (Rsqr (Rminus (Rmult l (cos a)) (Rmult (v V) (val T)))) (Rsqr (Rmult l (sin a)))) (Rsqr AlertRange) *)
intros.
(* Goal: Rle (Rplus (Rsqr (Rminus (Rmult l (cos a)) (Rmult (v V) (val T)))) (Rsqr (Rmult l (sin a)))) (Rsqr AlertRange) *)
cut (0 <= 2 * PI - a)%R.
(* Goal: forall _ : Rle (IZR Z0) (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a), Rle (Rplus (Rsqr (Rminus (Rmult l (cos a)) (Rmult (v V) (val T)))) (Rsqr (Rmult l (sin a)))) (Rsqr AlertRange) *)
(* Goal: Rle (IZR Z0) (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
cut (2 * PI - a <= MinBeta)%R.
(* Goal: forall (_ : Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) MinBeta) (_ : Rle (IZR Z0) (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a)), Rle (Rplus (Rsqr (Rminus (Rmult l (cos a)) (Rmult (v V) (val T)))) (Rsqr (Rmult l (sin a)))) (Rsqr AlertRange) *)
(* Goal: Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) MinBeta *)
(* Goal: Rle (IZR Z0) (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
cut (cos (2 * PI - a) = cos a).
(* Goal: forall (_ : @eq R (cos (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a)) (cos a)) (_ : Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) MinBeta) (_ : Rle (IZR Z0) (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a)), Rle (Rplus (Rsqr (Rminus (Rmult l (cos a)) (Rmult (v V) (val T)))) (Rsqr (Rmult l (sin a)))) (Rsqr AlertRange) *)
(* Goal: @eq R (cos (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a)) (cos a) *)
(* Goal: Rle (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) MinBeta *)
(* Goal: Rle (IZR Z0) (Rminus (Rmult (IZR (Zpos (xO xH))) PI) a) *)
cut (sin (2 * PI - a) = (- sin a)%R).
intros; rewrite Rsqr_mult; rewrite (Rsqr_neg (sin a)); rewrite <- H3;
 rewrite <- H4; rewrite <- Rsqr_mult;
 apply (Math_prop_alarm_1 (2 * PI - a) l T H H0 H6 H5).
replace (2 * PI - a)%R with (- a + 2 * INR 1 * PI)%R;
 [ rewrite (sin_period (- a) 1); apply sin_neg | simpl; ring ].
replace (2 * PI - a)%R with (- a + 2 * INR 1 * PI)%R;
 [ rewrite (cos_period (- a) 1); apply cos_neg | simpl; ring ].
generalize (Rplus_le_compat_l (MinBeta - a) (2 * PI - MinBeta) a H1);
 replace (MinBeta - a + (2 * PI - MinBeta))%R with (2 * PI - a)%R;
 [ replace (MinBeta - a + a)%R with MinBeta; [ intro; assumption | ring ]
 | ring ].
generalize (Rplus_le_compat_r (- a) a (2 * PI) H2); rewrite Rplus_opp_r;
(* Goal: Rle (IZR Z0) a *)
 intro; assumption.
Qed.
