proposition: Lemma fct_der3 : forall (eps : posreal) (t : R), derivable_pt (fun y : R => (Rsqr (xP y) + (Rsqr (yP y) + Rsqr eps))%R) t.
proof: Proof. intros; reg. apply yP_derivable. apply xP_derivable. Qed.
imports: Reals trajectory_const rrho trajectory_def constants