proposition: Lemma Rsqr_evader_distance_derivable : derivable Rsqr_evader_distance.
proof: Proof. unfold Rsqr_evader_distance in |- *. set (xi_p := xi intr); set (yi_p := yi intr); reg. apply (yi_derivable intr). apply (xi_derivable intr). Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega