proposition: Lemma yP_derive : forall t : R, derive_pt yP t (yP_derivable t) = derive_pt yi t (yi_derivable t).
proof: Proof. intro; unfold yP in |- *; reg. apply pr_nu. apply yi_derivable. Qed.
imports: Reals trajectory_const rrho trajectory_def constants