proposition: Theorem ails_alarm_at_alerting_distance : forall (intr : Trajectory) (evad : EvaderTrajectory), (d intr evad <= AlertRange)%R -> ails_alert (measure2state intr 0) (measure2state (tr evad) 0).
proof: Proof. Proof with trivial. intros; apply alarm_at_alerting_distance... Qed.
imports: Bool Reals trajectory_const trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory alarm alpha_no_conflict