proposition: Lemma Rsqr_intruder_distance_derivable : derivable Rsqr_intruder_distance.
proof: Proof. unfold Rsqr_intruder_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