proposition: Lemma derivative_eq_zero_tmin : forall (intruder evader : State) (t : R), (RR intruder evader (tmin intruder evader) <= RR intruder evader t)%R.
proof: Proof. intros; case (Req_EM_var (div_tau intruder evader) 0); intro. right; apply (R_equal_when_zero intruder evader (tmin intruder evader) t e). apply Rsqr_incr_0. repeat rewrite R_Rmin. apply Rplus_le_compat_r; apply Rmult_le_compat_l. apply Ax2_R_pos. unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rsqr_0; apply Rle_0_sqr. assumption. assumption. apply RR_pos. apply RR_pos. Qed.
imports: Reals ails_def trajectory_const