proposition: Lemma asymptotic_decrease_tau : forall (intruder evader : State) (t t1 t2 : R), (t2 <= tau intruder evader t)%R -> (t1 <= t2)%R -> (RR intruder evader (t + t2) <= RR intruder evader (t + t1))%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 t n) in H; apply asymptotic_decrease_tmin; [ apply Rplus_le_reg_l with (- t)%R; repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; rewrite Rplus_comm; assumption | apply (Rplus_le_compat_l t t1 t2 H0) ] ]. Qed.
imports: Reals ails_def trajectory_const