proposition: Lemma xP_derive : forall t : R, derive_pt xP t (xP_derivable t) = derive_pt xi t (xi_derivable t).
proof: Proof. intro; unfold xP in |- *; reg. apply pr_nu. apply xi_derivable. Qed.
imports: Reals trajectory_const rrho trajectory_def constants