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