proposition: Lemma no_conflict_Omega_t : forall t : R, (ConflictRange + vi intr < l)%R -> (0 <= t)%R -> (rho_vi * t <= PI - rho_vi)%R -> Omega (beta + thetat intr 0) = true -> (ConflictRange < e t)%R.
proof: Proof. intros; case (Rle_dec 1 t); intro. apply Rsqr_incrst_0. unfold e in |- *; rewrite Rsqr_sqrt. apply (no_conflict_scenario_1_Omega t r H1 H2). apply Rsqr_evader_distance_pos. left; unfold ConflictRange in |- *; prove_sup. unfold e in |- *; apply sqrt_positivity; apply Rsqr_evader_distance_pos. cut (t < 1)%R. intro; apply (no_conflict_scenario_0_1s t H0 H3 H). auto with real. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega