fact: Definition tau (intruder evader : State) (t : R) : R := match Req_EM_var (div_tau intruder evader) 0 with | left _ => 0%R | right _ => (- (dx intruder evader t * dxdt intruder + dy intruder evader t * dydt intruder) / div_tau intruder evader)%R end.
imports: Reals ails_def trajectory_const