proposition: Lemma R_distance : forall intruder evader : State, RR intruder evader 0 = distance intruder evader.
proof: Proof. Proof with trivial. intros; unfold RR, distance in |- *; unfold dx, dy in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rplus_0_r; rewrite (Rsqr_neg (xt intruder - xt evader)); rewrite (Rsqr_neg (yt intruder - yt evader)); repeat rewrite Ropp_minus_distr... Qed.
imports: Reals trajectory_const constants ails_def tau Omega