proposition: Lemma L_intruder : forall t : R, (l <= e t + i t)%R.
proof: Proof. intro; apply Rsqr_incr_0. rewrite Rsqr_plus. cut (Rsqr l = (Rsqr (e t) + Rsqr (i t) + 2 * ((xe - xi intr t) * (xi intr t - xi intr 0) + (ye - yi intr t) * (yi intr t - yi intr 0)))%R). intro. rewrite H. apply Rplus_le_compat_l. repeat rewrite Rmult_assoc. apply Rmult_le_compat_l. left; prove_sup0. unfold e, i in |- *. unfold Rsqr_evader_distance, Rsqr_intruder_distance in |- *. rewrite (Rsqr_neg (xi intr t - xe)). rewrite (Rsqr_neg (yi intr t - ye)). replace (- (xi intr t - xe))%R with (xe - xi intr t)%R. replace (- (yi intr t - ye))%R with (ye - yi intr t)%R. apply sqrt_cauchy. ring. ring. rewrite L. unfold e, i in |- *. repeat rewrite Rsqr_sqrt. unfold Rsqr_evader_distance, Rsqr_intruder_distance in |- *. replace (xe - xi intr 0)%R with (xe - xi intr t + (xi intr t - xi intr 0))%R. replace (ye - yi intr 0)%R with (ye - yi intr t + (yi intr t - yi intr 0))%R. repeat rewrite Rsqr_plus. rewrite (Rsqr_neg (xe - xi intr t)). rewrite (Rsqr_neg (ye - yi intr t)). replace (- (xe - xi intr t))%R with (xi intr t - xe)%R. replace (- (ye - yi intr t))%R with (yi intr t - ye)%R. ring. ring. ring. ring. ring. apply Rsqr_intruder_distance_pos. apply Rsqr_evader_distance_pos. unfold l in |- *; unfold Die in |- *. apply sqrt_positivity. apply Rplus_le_le_0_compat; apply Rle_0_sqr. unfold e, i in |- *; apply Rplus_le_le_0_compat; apply sqrt_positivity. apply Rsqr_evader_distance_pos. apply Rsqr_intruder_distance_pos. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega