proposition: Lemma Alpha_d_AlertRange_2 : Alpha (beta intr evad T) = false -> (AlertRange < d intr evad)%R.
proof: Proof. Proof with trivial. unfold Alpha in |- *; case (Rle_dec ((Rsqr (ve evad * T) + Rsqr (l intr evad T) - Rsqr AlertRange) / (2 * ve evad * T)) (l intr evad T * cos (beta intr evad T))); intros... elim diff_true_false... unfold Rdiv in n; cut (0 < 2 * ve evad * T)%R... intro... cut (l intr evad T * cos (beta intr evad T) < (Rsqr (ve evad * T) + Rsqr (l intr evad T) - Rsqr AlertRange) * / (2 * ve evad * T))%R... intro; generalize (Rmult_lt_compat_r (2 * ve evad * T) (l intr evad T * cos (beta intr evad T)) ((Rsqr (ve evad * T) + Rsqr (l intr evad T) - Rsqr AlertRange) * / (2 * ve evad * T)) H0 H1); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... rewrite Rmult_1_r; intro; generalize (Rplus_lt_compat_l (Rsqr AlertRange - 2 * l intr evad T * ve evad * T * cos (beta intr evad T)) (l intr evad T * (cos (beta intr evad T) * (2 * (ve evad * T)))) (Rsqr (ve evad * T) + Rsqr (l intr evad T) - Rsqr AlertRange) H2); replace (Rsqr AlertRange - 2 * l intr evad T * ve evad * T * cos (beta intr evad T) + l intr evad T * (cos (beta intr evad T) * (2 * (ve evad * T))))%R with (Rsqr AlertRange)... replace (Rsqr AlertRange - 2 * l intr evad T * ve evad * T * cos (beta intr evad T) + (Rsqr (ve evad * T) + Rsqr (l intr evad T) - Rsqr AlertRange))%R with (Rsqr (ve evad * T) + Rsqr (l intr evad T) - 2 * ve evad * T * l intr evad T * cos (beta intr evad T))%R... rewrite <- d_l_beta... intro; apply Rsqr_incrst_0... left; apply AlertRange_pos... unfold d in |- *; unfold Die in |- *; apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr... ring... ring... repeat apply prod_neq_R0... discrR... red in |- *; intro; generalize (TypeSpeed_pos (h (tr evad))); intro; unfold ve in H2; rewrite H2 in H3; elim (Rlt_irrefl 0 H3)... cut (0 < T)%R... intro... red in |- *; intro; rewrite H3 in H2; elim (Rlt_irrefl 0 H2)... apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 T)... auto with real... repeat apply Rmult_lt_0_compat... prove_sup0... unfold ve in |- *; apply (TypeSpeed_pos (h (tr evad)))... apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 T)... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory alarm