proposition: Lemma D_Rs_2 : forall t : R, (derive_pt Rs t (Rs_derivable t) * (2 * derive_pt alphas t (cond_D1 alphas t) - derive_pt thetat t (thetat_derivable t)))%R = (- Rs t * derive_pt (derive alphas (cond_D1 alphas)) t (cond_D2 alphas t))%R.
proof: Proof. intro. assert (H := D_Rs_alphas1 t). assert (H0 := D_Rs_alphas2 t). assert (H1 := DRs t). rewrite H in H0; rewrite <- H1 in H0. assert (H2 := Rplus_eq_compat_l (- derive_pt Rs t (Rs_derivable t) * (derive_pt thetat t (thetat_derivable t) - derive_pt alphas t (cond_D1 alphas t)) + - Rs t * derive_pt (derive alphas (cond_D1 alphas)) t (cond_D2 alphas t)) _ _ H0). cut ((- derive_pt Rs t (Rs_derivable t) * (derive_pt thetat t (thetat_derivable t) - derive_pt alphas t (cond_D1 alphas t)) + - Rs t * derive_pt (derive alphas (cond_D1 alphas)) t (cond_D2 alphas 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 = (derive_pt Rs t (Rs_derivable t) * (2 * derive_pt alphas t (cond_D1 alphas t) - derive_pt thetat t (thetat_derivable t)))%R); [ intro | ring ]. cut ((- derive_pt Rs t (Rs_derivable t) * (derive_pt thetat t (thetat_derivable t) - derive_pt alphas t (cond_D1 alphas t)) + - Rs t * derive_pt (derive alphas (cond_D1 alphas)) t (cond_D2 alphas t) + derive_pt Rs t (Rs_derivable t) * (derive_pt thetat t (thetat_derivable t) - derive_pt alphas t (cond_D1 alphas t)))%R = (- Rs t * derive_pt (derive alphas (cond_D1 alphas)) t (cond_D2 alphas t))%R); [ intro | ring ]. rewrite H3 in H2; rewrite H4 in H2. assumption. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho