proposition: Lemma YCNGFTYS_evader : forall t : R, (0 <= t)%R -> (l - v (vi intr) * t <= e t)%R.
proof: Proof. intros; cut (i t <= vi intr * t)%R; [ intros; unfold Rminus in |- *; rewrite Rplus_comm; apply Rplus_le_reg_l with (vi intr * t)%R; repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l; rewrite Rplus_comm; apply Rle_trans with (e t + i t)%R; [ apply L_intruder | apply Rplus_le_compat_l; assumption ] | unfold i in |- *; unfold Rsqr_intruder_distance in |- *; apply (YCNGFTYS intr t H) ]. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega