proposition: Lemma fct_der5 : forall t : R, derivable_pt (fun y : R => (Rs y * derive_pt alphas y (cond_D1 alphas y))%R) t.
proof: Proof. intro; set (alpha_p := d2 alphas); set (f := fun x : R => derive_pt alpha_p x (cond_D1 alphas x)). change (derivable_pt (fun y : R => (Rs y * f y)%R) t) in |- *. reg. apply (cond_D2 alphas). apply Rs_derivable. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho