proposition: Lemma RR_pos : forall (intruder evader : State) (t : R), (0 <= RR intruder evader t)%R.
proof: Proof. intros; unfold RR in |- *; apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr. Qed.
imports: Reals ails_def trajectory_const