proposition: Lemma R_T_d_diff_0 : h (tr evad) = V -> (0 < l intr evad T)%R -> (d intr evad <= RR (measure2state intr 0) (measure2state (tr evad) 0) T)%R -> (cos (beta intr evad T + thetat intr 0) <= cos (beta intr evad T))%R.
proof: Proof. Proof with trivial. intros hyp_evad H... cut (0 <= d intr evad)%R... cut (0 <= RR (measure2state intr 0) (measure2state (tr evad) 0) T)%R... intros... generalize (Rsqr_incr_1 _ (RR (measure2state intr 0) (measure2state (tr evad) 0) T) H2 H1 H0); intro... rewrite R_T in H3... rewrite (d_l_beta intr evad T) in H3... unfold ve in H3... rewrite hyp_evad in H3... rewrite Rsqr_minus in H3... repeat rewrite Rsqr_mult in H3... rewrite cos2 in H3... generalize (Rplus_le_compat_l (- Rsqr (l intr evad T) - Rsqr V * Rsqr T) (Rsqr V * Rsqr T + Rsqr (l intr evad T) - 2 * V * T * l intr evad T * cos (beta intr evad T)) (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))) H3)... replace (- Rsqr (l intr evad T) - Rsqr V * Rsqr T + (Rsqr V * Rsqr T + Rsqr (l intr evad T) - 2 * V * T * l intr evad T * cos (beta intr evad T)))%R with (2 * V * T * l intr evad T * - cos (beta intr evad T))%R... replace (- Rsqr (l intr evad T) - Rsqr V * Rsqr T + (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 (2 * V * T * l intr evad T * - cos (beta intr evad T + thetat intr 0))%R... intro... rewrite <- (Ropp_involutive (cos (beta intr evad T)))... rewrite <- (Ropp_involutive (cos (beta intr evad T + thetat intr 0)))... apply Ropp_ge_le_contravar... apply Rle_ge... apply Rmult_le_reg_l with (2 * V * T * l intr evad T)%R... apply Rmult_lt_0_compat... prove_sup0... apply Rlt_le_trans with MinT; [ apply MinT_is_pos | apply (cond_1 T) ]... ring... ring... apply RR_pos... unfold d in |- *; unfold Die in |- *; apply sqrt_positivity... apply Rplus_le_le_0_compat; apply Rle_0_sqr... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory alarm