proposition: Lemma YCNGSTYS_evader : forall t : R, (0 <= t)%R -> (rho_vi * t < 2)%R -> (2 * r_vi * sin (rho_vi * (t / 2)) - l <= e t)%R.
proof: Proof. intros; cut (2 * r_vi * sin (rho_vi * (t / 2)) <= i t)%R; [ intro; intros; unfold Rminus in |- *; rewrite Rplus_comm; apply Rplus_le_reg_l with l; repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_l; apply Rle_trans with (i t); [ assumption | apply L_i ] | unfold i in |- *; unfold Rsqr_intruder_distance in |- *; apply (YCNGSTYS intr t H H0) ]. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega