proposition: Lemma D_G_alphas : forall t : R, (derive_pt G t (G_derivable t) * (derive_pt Rs t (Rs_derivable t) + derive_pt F t (F_derivable t)))%R = (- Rsqr (derive_pt alphas t (cond_D1 alphas t)) * G t * (Rs t + F t) + Rsqr (F t) * (Rsqr (rho (vi intr) / 2) - Rsqr (derive_pt alphas t (cond_D1 alphas t))))%R.
proof: Proof. intro. cut (derive_pt G t (G_derivable t) = (derive_pt Rs t (Rs_derivable t) - derive_pt F t (F_derivable t))%R). intro; rewrite H; rewrite (Rsqr_minus_plus (derive_pt Rs t (Rs_derivable t)) (derive_pt F t (F_derivable t))); unfold G in |- *; repeat rewrite Rmult_assoc; rewrite (Rsqr_minus_plus (Rs t) (F t)). replace (- Rsqr (derive_pt alphas t (cond_D1 alphas t)) * (Rsqr (Rs t) - Rsqr (F t)) + Rsqr (F t) * (Rsqr (rho (vi intr) / 2) - Rsqr (derive_pt alphas t (cond_D1 alphas t))))%R with (- Rsqr (derive_pt alphas t (cond_D1 alphas t)) * Rsqr (Rs t) + Rsqr (F t) * Rsqr (rho (vi intr) / 2))%R. apply Rplus_eq_reg_l with (Rsqr (derive_pt F t (F_derivable t)) + Rsqr (derive_pt alphas t (cond_D1 alphas t)) * Rsqr (Rs t))%R. replace (Rsqr (derive_pt F t (F_derivable t)) + Rsqr (derive_pt alphas t (cond_D1 alphas t)) * Rsqr (Rs t) + (Rsqr (derive_pt Rs t (Rs_derivable t)) - Rsqr (derive_pt F t (F_derivable t))))%R with (Rsqr (derive_pt Rs t (Rs_derivable t)) + Rsqr (Rs t) * Rsqr (derive_pt alphas t (cond_D1 alphas t)))%R. replace (Rsqr (derive_pt F t (F_derivable t)) + Rsqr (derive_pt alphas t (cond_D1 alphas t)) * Rsqr (Rs t) + (- Rsqr (derive_pt alphas t (cond_D1 alphas t)) * Rsqr (Rs t) + Rsqr (F t) * Rsqr (rho (vi intr) / 2)))%R with (Rsqr (derive_pt F t (F_derivable t)) + Rsqr (rho (vi intr) / 2) * Rsqr (F t))%R. rewrite Rsqr_DRs; rewrite D_F_Rsqr_v; reflexivity. ring. ring. ring. unfold G in |- *. cut (derivable_pt Rs t); [ intro X | apply Rs_derivable ]. cut (derivable_pt F t); [ intro X0 | apply F_derivable ]. reg. replace (derive_pt F t (F_derivable 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