proposition: Lemma D_Rs_alphas1 : forall t : R, derive_pt (fun y : R => (Rs y * derive_pt alphas y (cond_D1 alphas y))%R) t (fct_der5 t) = (derive_pt Rs t (Rs_derivable t) * derive_pt alphas t (cond_D1 alphas t) + Rs t * derive_pt (derive alphas (cond_D1 alphas)) t (cond_D2 alphas t))%R.
proof: Proof. intro. set (f := fun x : R => derive_pt alphas x (cond_D1 alphas x)). replace (derive_pt (fun y : R => (Rs y * derive_pt alphas y (cond_D1 alphas y))%R) t (fct_der5 t)) with (derive_pt (fun y : R => (Rs y * f y)%R) t (fct_der5 t)); [ idtac | reflexivity ]. replace (derive_pt alphas t (cond_D1 alphas t)) with (f t); [ idtac | reflexivity ]. replace (derive_pt (derive alphas (cond_D1 alphas)) t (cond_D2 alphas t)) with (derive_pt f t (cond_D2 alphas t)); [ idtac | reflexivity ]. cut (derivable_pt Rs t); [ intro X | apply Rs_derivable ]. cut (derivable_pt f t); [ intro X0 | apply (cond_D2 alphas) ]. reg. replace (derive_pt f t (cond_D2 alphas t)) with (derive_pt f t X0); [ idtac | apply pr_nu ]. replace (derive_pt Rs t (Rs_derivable t)) with (derive_pt Rs t X); [ idtac | apply pr_nu ]. ring. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho