proposition: Lemma step1 : forall evader intruder : State, alerting_distance evader intruder -> chktrack intruder evader 0.
proof: Proof. Proof with trivial. intros; unfold alerting_distance in H; unfold chktrack in |- *; case (Rle_dec (tau intruder evader 0) 0); intro... unfold chkrange in |- *; split... rewrite R_distance; rewrite distance_sym... unfold AlertTime in |- *; left; prove_sup... case (Rlt_dec AlertTime (0 + tau intruder evader 0)); intro... rewrite Rplus_0_l in r; cut (0 <= AlertTime)%R... intro; assert (H1 := asymptotic_decrease_tau intruder evader 0 0 AlertTime (Rlt_le AlertTime (tau intruder evader 0) r) H0); repeat rewrite Rplus_0_l in H1; rewrite R_distance in H1; rewrite distance_sym in H1; apply Rle_trans with (distance evader intruder)... unfold AlertTime in |- *; left; prove_sup... assert (H0 := derivative_eq_zero_min intruder evader 0 0); repeat rewrite Rplus_0_l in H0; rewrite R_distance in H0; rewrite distance_sym in H0; apply Rle_trans with (distance evader intruder)... Qed.
imports: Reals trajectory_const constants ails_def tau Omega