proposition: Lemma fct_der2 : forall (eps : posreal) (t : R), derivable_pt (fun y : R => Rsqr (u eps y)) t.
proof: Proof. intros; set (f := u eps); reg. apply (d_u eps). Qed.
imports: Reals trajectory_const rrho trajectory_def constants