proposition: Lemma isometric_evader : forall t : R, Rsqr_evader_distance t = (Rsqr (xp t) + Rsqr (yp t))%R.
proof: Proof. intro; unfold Rsqr_evader_distance, xp, yp in |- *; repeat rewrite Rsqr_plus; ring_simplify; repeat rewrite Rsqr_mult; rewrite <- (Rsqr_neg (sin (thetat intr 0))); pattern (Rsqr (xi intr t - xe)) at 1 in |- *. replace (Rsqr (xi intr t - xe)) with ((Rsqr (sin (thetat intr 0)) + Rsqr (cos (thetat intr 0))) * Rsqr (xi intr t - xe))%R. pattern (Rsqr (yi intr t - ye)) at 1 in |- *. replace (Rsqr (yi intr t - ye)) with ((Rsqr (sin (thetat intr 0)) + Rsqr (cos (thetat intr 0))) * Rsqr (yi intr t - ye))%R. ring. rewrite sin2_cos2 in |- *; ring. rewrite sin2_cos2 in |- *; ring. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega