proposition: Lemma asymptotic_decrease_tmin : forall (intruder evader : State) (t1 t2 : R), (t2 <= tmin intruder evader)%R -> (t1 <= t2)%R -> (RR intruder evader t2 <= RR intruder evader t1)%R.
proof: Proof. intros; case (Req_EM_var (div_tau intruder evader) 0); intro. right; apply (R_equal_when_zero intruder evader t2 t1 e). apply Rsqr_incr_0. repeat rewrite R_Rmin. apply Rplus_le_compat_r; apply Rmult_le_compat_l. apply Ax2_R_pos. case (Rtotal_order (tmin intruder evader) t1); intro. generalize (Rle_lt_trans t2 (tmin intruder evader) t1 H H1); intro; elim (Rlt_irrefl t1 (Rle_lt_trans t1 t2 t1 H0 H2)). elim H1; intros. rewrite H2 in H; generalize (Rle_antisym t1 t2 H0 H); intro; rewrite H3; right; reflexivity. rewrite Rsqr_neg; rewrite (Rsqr_neg (t1 - tmin intruder evader)); replace (- (t2 - tmin intruder evader))%R with (tmin intruder evader - t2)%R. replace (- (t1 - tmin intruder evader))%R with (tmin intruder evader - t1)%R. apply Rsqr_incr_1. unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_ge_le_contravar; apply Rle_ge; assumption. apply Rplus_le_reg_l with t2; 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 t1; 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 t2; assumption. ring. ring. assumption. assumption. apply RR_pos. apply RR_pos. Qed.
imports: Reals ails_def trajectory_const