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