proposition: Lemma isometric_intruder : forall t : R, Rsqr_intruder_distance t = (Rsqr (xp t - xp 0) + Rsqr (yp t - yp 0))%R.
proof: Proof. intro; unfold Rsqr_intruder_distance in |- *; rewrite xpt_xp0; rewrite ypt_yp0; repeat rewrite Rsqr_plus; ring_simplify; repeat rewrite Rsqr_mult; rewrite <- Rsqr_neg. pattern (Rsqr (xi intr t - xi intr 0)) at 1 in |- *. replace (Rsqr (xi intr t - xi intr 0)) with ((Rsqr (sin (thetat intr 0)) + Rsqr (cos (thetat intr 0))) * Rsqr (xi intr t - xi intr 0))%R. pattern (Rsqr (yi intr t - yi intr 0)) at 1 in |- *. replace (Rsqr (yi intr t - yi intr 0)) with ((Rsqr (sin (thetat intr 0)) + Rsqr (cos (thetat intr 0))) * Rsqr (yi intr t - yi intr 0))%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