proposition: Lemma asymptotic_tau_gt : forall (intruder evader : State) (t dt : R), (0 <= dt)%R -> (RR intruder evader (t + dt) < RR intruder evader t)%R -> (0 < tau intruder evader t)%R.
proof: Proof. intros; case (Rtotal_order 0 (tau intruder evader t)); intro; [ assumption | cut (tau intruder evader t <= 0)%R; [ intro; elim H1; intro; generalize (asymptotic_increase_tau intruder evader t 0 dt H2 H); rewrite Rplus_0_r; intro; elim (Rlt_irrefl (RR intruder evader t) (Rle_lt_trans (RR intruder evader t) (RR intruder evader (t + dt)) (RR intruder evader t) H4 H0)) | elim H1; intro; [ right; symmetry in |- *; assumption | left; assumption ] ] ]. Qed.
imports: Reals ails_def trajectory_const