proposition: Lemma majoration : forall t : R, (Rsqr (yp t) <= Rsqr_evader_distance t)%R /\ (Rsqr (xp t) <= Rsqr_evader_distance t)%R.
proof: Proof. intro; generalize (isometric_evader t); intro; split; [ rewrite H; pattern (Rsqr (yp t)) at 1 in |- *; rewrite <- (Rplus_0_l (Rsqr (yp t))); apply Rplus_le_compat_r; apply Rle_0_sqr | rewrite H; pattern (Rsqr (xp t)) at 1 in |- *; rewrite <- (Rplus_0_r (Rsqr (xp t))); apply Rplus_le_compat_l; apply Rle_0_sqr ]. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega