proposition: Lemma tau_equal_when_zero : forall (intruder evader : State) (t : R), div_tau intruder evader = 0%R -> tau intruder evader t = 0%R.
proof: Proof. intros; unfold tau in |- *; case (Req_EM_var (div_tau intruder evader) 0); intro; [ reflexivity | elim n; exact H ]. Qed.
imports: Reals ails_def trajectory_const