proposition: Lemma Alpha_d_AlertRange_3 : (AlertRange < d intr evad)%R -> Alpha (beta intr evad T) = false.
proof: Proof. Proof with trivial. intros; 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))); intro... unfold Rdiv in r; cut (0 < 2 * ve evad * T)%R... intro; generalize (Rmult_le_compat_l (2 * ve evad * T) ((Rsqr (ve evad * T) + Rsqr (l intr evad T) - Rsqr AlertRange) * / (2 * ve evad * T)) (l intr evad T * cos (beta intr evad T)) (Rlt_le 0 (2 * ve evad * T) H0) r)... rewrite <- (Rmult_comm ((Rsqr (ve evad * T) + Rsqr (l intr evad T) - Rsqr AlertRange) * / (2 * ve evad * T))); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... rewrite Rmult_1_r; intro... generalize (Rplus_le_compat_l (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) (2 * (ve evad * (T * (l intr evad T * cos (beta intr evad T))))) H1)... 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; replace (Rsqr AlertRange - 2 * l intr evad T * ve evad * T * cos (beta intr evad T) + 2 * (ve evad * (T * (l intr evad T * cos (beta intr evad T)))))%R with (Rsqr AlertRange)... intro... generalize (Rsqr_incr_0_var (d intr evad) AlertRange H2 (Rlt_le 0 AlertRange AlertRange_pos))... intro... elim (Rlt_irrefl (d intr evad) (Rle_lt_trans _ _ _ H3 H))... ring... ring... repeat apply prod_neq_R0... discrR... red in |- *; intro; generalize (TypeSpeed_pos (h (tr evad))); intro; unfold ve in H1; rewrite H1 in H2; elim (Rlt_irrefl 0 H2)... cut (0 < T)%R... intro... red in |- *; intro; rewrite H2 in H1; elim (Rlt_irrefl 0 H1)... apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 T)... 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