proposition: Theorem no_conflict_Omega : (ConflictRange + v (vi intr) < l)%R -> (rho_vi * T <= PI - rho_vi)%R -> Omega (beta + thetat intr 0) = true -> 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_Omega_t T H H2 H0 H1); intro; cut (e T = Die T T)... intro; rewrite H4 in H3; elim (Rlt_irrefl (Die T T) (Rle_lt_trans (Die T T) ConflictRange (Die T T) r H3))... 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