proposition: Lemma d_distance : forall (intr : Trajectory) (evad : EvaderTrajectory), distance (measure2state (tr evad) 0) (measure2state intr 0) = d intr evad.
proof: Proof. Proof with trivial. unfold distance, d in |- *; unfold Die in |- *; simpl in |- *; unfold xi, yi in |- *... Qed.
imports: Reals trajectory_const trajectory_def constants ycngftys ycngstys tau ails trajectory measure2state