proposition: Lemma tau_gt_time : forall (intruder evader : State) (t1 t2 t : R), (t < tau intruder evader t2)%R -> (t1 <= t2)%R -> (t < tau intruder evader t1)%R.
proof: Proof. intros. case (Req_EM_var (div_tau intruder evader) 0); intro. rewrite (tau_equal_when_zero intruder evader t1 e). rewrite (tau_equal_when_zero intruder evader t2 e) in H. assumption. cut (t1 = (t2 + (t1 - t2))%R). intro. rewrite H1. rewrite (tau_is_uniform intruder evader t2 (t1 - t2) n). unfold Rminus in |- *. cut (0 <= - (t1 - t2))%R. intro. generalize (Rplus_lt_le_compat t (tau intruder evader t2) 0 (- (t1 - t2)) H H2). rewrite Rplus_0_r. intro; assumption. rewrite <- Ropp_0. apply Ropp_ge_le_contravar. apply Rle_ge. apply Rplus_le_reg_l with t2. rewrite <- H1; rewrite Rplus_0_r; assumption. ring. Qed.
imports: Reals ails_def trajectory_const