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