proposition: Lemma dx_dxdt : forall (intruder evader : State) (t : R), (xt intruder - xt evader + t * dxdt intruder)%R = dx intruder evader t.
proof: Proof. intros; unfold dxdt, dx in |- *; ring. Qed.
imports: Reals ails_def trajectory_const