proposition: Lemma asymptotic_increase_tmin : forall (intruder evader : State) (t1 t2 : R), (tmin intruder evader <= t1)%R -> (t1 <= t2)%R -> (RR intruder evader t1 <= RR intruder evader t2)%R.
proof: Proof. intros; case (Req_EM_var (div_tau intruder evader) 0); intro. right; apply (R_equal_when_zero intruder evader t1 t2 e). apply Rsqr_incr_0. repeat rewrite R_Rmin. apply Rplus_le_compat_r; apply Rmult_le_compat_l. apply Ax2_R_pos. apply Rsqr_incr_1. unfold Rminus in |- *; apply Rplus_le_compat_r; assumption. apply Rplus_le_reg_l with (tmin intruder evader); rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *; repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; assumption. apply Rplus_le_reg_l with (tmin intruder evader); rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *; repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply Rle_trans with t1; assumption. assumption. assumption. apply RR_pos. apply RR_pos. Qed.
imports: Reals ails_def trajectory_const