proposition: Lemma L_i : forall t : R, (i t <= l + e t)%R.
proof: Proof. intro. apply Rsqr_incr_0. rewrite Rsqr_plus. cut (Rsqr (i t) = (Rsqr l + Rsqr (e t) + 2 * ((xi intr t - xe) * (xe - xi intr 0) + (yi intr t - ye) * (ye - yi intr 0)))%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 e in |- *. unfold Rsqr_evader_distance in |- *. rewrite <- (Rmult_comm (sqrt (Rsqr (xi intr t - xe) + Rsqr (yi intr t - ye)))) . apply sqrt_cauchy. 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 - xi intr 0)%R with (xi intr t - xe + (xe - xi intr 0))%R. replace (yi intr t - yi intr 0)%R with (yi intr t - ye + (ye - yi intr 0))%R. repeat rewrite Rsqr_plus. ring. ring. ring. apply Rsqr_evader_distance_pos. apply Rsqr_intruder_distance_pos. unfold i in |- *. apply sqrt_positivity. apply Rsqr_intruder_distance_pos. apply Rplus_le_le_0_compat. apply l_is_pos. unfold e in |- *. apply sqrt_positivity. apply Rsqr_evader_distance_pos. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega