proposition: Lemma dy_dydt : forall (intruder evader : State) (t : R), (yt intruder - yt evader + t * dydt intruder)%R = dy intruder evader t.
proof: Proof. intros; unfold dydt, dy in |- *; ring. Qed.
imports: Reals ails_def trajectory_const