proposition: Lemma R_T_d_diff_1 : h (tr evad) = V -> (cos (beta intr evad T + thetat intr 0) <= cos (beta intr evad T))%R -> (d intr evad <= RR (measure2state intr 0) (measure2state (tr evad) 0) T)%R.
proof: Proof. Proof with trivial. intros... apply Rsqr_incr_0... rewrite R_T... rewrite (d_l_beta intr evad T)... unfold ve in |- *... rewrite H... rewrite Rsqr_minus... repeat rewrite Rsqr_mult... rewrite cos2... replace (Rsqr (l intr evad T) * (1 - Rsqr (sin (beta intr evad T + thetat intr 0))) + Rsqr V * Rsqr T - 2 * (l intr evad T * cos (beta intr evad T + thetat intr 0)) * (V * T) + Rsqr (l intr evad T) * Rsqr (sin (beta intr evad T + thetat intr 0)))%R with (Rsqr V * Rsqr T + Rsqr (l intr evad T) - 2 * (l intr evad T * cos (beta intr evad T + thetat intr 0)) * (V * T))%R... unfold Rminus in |- *... apply Rplus_le_compat_l... apply Ropp_ge_le_contravar... apply Rle_ge... repeat rewrite Rmult_assoc... apply Rmult_le_compat_l... left; prove_sup0... rewrite <- (Rmult_comm (V * T))... rewrite (Rmult_comm (l intr evad T))... repeat rewrite Rmult_assoc... apply Rmult_le_compat_l... left; apply TypeSpeed_pos... apply Rmult_le_compat_l... left; apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ]... rewrite <- (Rmult_comm (l intr evad T))... apply Rmult_le_compat_l... apply l_is_pos... unfold Rminus in |- *... rewrite Rmult_plus_distr_l... ring... unfold d in |- *; unfold Die in |- *; apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr... apply RR_pos... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory alarm