proposition: Lemma no_conflict_scenario_0_1s : forall t : R, (0 <= t)%R -> (t < 1)%R -> (ConflictRange + vi intr < l)%R -> (ConflictRange < e t)%R.
proof: Proof. Proof with trivial. intros; apply Rlt_le_trans with (l - vi intr * t)%R... apply Rplus_lt_reg_l with (v (vi intr)); rewrite <- (Rplus_comm ConflictRange); apply Rlt_trans with l... apply Rplus_lt_reg_l with (- l)%R; rewrite Rplus_opp_l; replace (- l + (vi intr + (l - vi intr * t)))%R with (vi intr * (1 - t))%R... apply Rmult_lt_0_compat... apply TypeSpeed_pos... generalize (Rplus_lt_compat_r (- t) t 1 H0); rewrite Rplus_opp_r... unfold Rminus in |- *; rewrite Rmult_plus_distr_l; ring... apply (YCNGFTYS_evader t H)... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega