proposition: Lemma no_conflict_scenario_1_Omega : forall t : R, (1 <= t)%R -> (rho_vi * t <= PI - rho_vi)%R -> Omega (beta + thetat intr 0) = true -> (Rsqr ConflictRange < Rsqr_evader_distance t)%R.
proof: Proof. Proof with trivial. intros; apply Rlt_le_trans with (Rsqr (xp t))... apply Rsqr_incrst_1... apply (no_conflict_xp_1_Omega t H H0 H1)... unfold ConflictRange in |- *; left; prove_sup... cut ((0 <= t)%R /\ (rho_vi * t <= PI)%R)... intro; elim H2; intros; apply (xp_pos t H3 H4 H1)... split... left; apply Rlt_le_trans with 1%R; try apply Rlt_0_1... unfold Rminus in H0; generalize (Rplus_le_compat_r rho_vi (rho_vi * t) (PI + - rho_vi) H0); repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; intro; apply (plus_le_is_le (rho_vi * t) rho_vi PI)... unfold rho_vi in |- *; left; apply rho_pos... elim (majoration t)... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega