proposition: Lemma no_conflict_lt_min_t : forall t : R, let MinDistance := (2 * r_vi * sin (rho_vi * (t / 2)) - ConflictRange)%R in (0 <= t)%R -> (0 <= rho_vi * t)%R -> (rho_vi * t < 2)%R -> (l < MinDistance)%R -> (ConflictRange < e t)%R.
proof: Proof. Proof with trivial. intros; apply Rlt_le_trans with (2 * r_vi * sin (rho_vi * (t / 2)) - l)%R... unfold MinDistance in H2; apply Rplus_lt_reg_l with (- ConflictRange + l)%R; replace (- ConflictRange + l + ConflictRange)%R with l... replace (- ConflictRange + l + (2 * r_vi * sin (rho_vi * (t / 2)) - l))%R with (2 * r_vi * sin (rho_vi * (t / 2)) - ConflictRange)%R; try ring... ring... apply (YCNGSTYS_evader t H H1)... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega