proposition: Lemma no_conflict_gt_max_t : forall t : R, let MaxDistance := (vi intr * t + ConflictRange)%R in (0 <= t)%R -> (MaxDistance < l)%R -> (ConflictRange < e t)%R.
proof: Proof. Proof with trivial. intros; apply Rlt_le_trans with (l - vi intr * t)%R... unfold MaxDistance in H0; rewrite Rplus_comm in H0; generalize (Rplus_lt_compat_r (- (vi intr * t)) (ConflictRange + vi intr * t) l H0); repeat rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r... apply (YCNGFTYS_evader t H)... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega