proposition: Lemma derivative_eq_zero_min : forall (intruder evader : State) (t1 t2 : R), (RR intruder evader (t1 + tau intruder evader t1) <= RR intruder evader (t1 + t2))%R.
proof: Proof. intros; case (Req_EM_var (div_tau intruder evader) 0); intro; [ right; apply R_equal_when_zero; assumption | rewrite (tau_tmin intruder evader t1 n); replace (t1 + (tmin intruder evader - t1))%R with (tmin intruder evader); [ apply derivative_eq_zero_tmin | ring ] ]. Qed.
imports: Reals ails_def trajectory_const