proposition: Lemma conflict_T_e_1 : (e T <= ConflictRange)%R -> conflict T = true.
proof: Proof. Proof with trivial. intro; cut (e T = Die T T)... intro; rewrite H0 in H; unfold conflict in |- *; case (Rle_dec (Die T T) ConflictRange); intro... elim n; assumption... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega