proposition: Theorem no_conflict_gt_max : let MaxDistance := (vi intr * T + ConflictRange)%R in (MaxDistance < l)%R -> conflict T = false.
proof: Proof. Proof with trivial. intros; unfold conflict in |- *; case (Rle_dec (Die T T) ConflictRange); intro... cut (0 <= T)%R... intro; generalize (no_conflict_gt_max_t T H0 H); intro; cut (e T = Die T T)... intro; rewrite H2 in H1; elim (Rlt_irrefl (Die T T) (Rle_lt_trans (Die T T) ConflictRange (Die T T) r H1))... left; apply Rlt_le_trans with MinT... apply MinT_is_pos... apply (cond_1 T)... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega