proposition: Lemma Rsqr_DRs : forall t : R, (Rsqr (derive_pt Rs t (Rs_derivable t)) + Rsqr (Rs t) * Rsqr (derive_pt alphas t (cond_D1 alphas t)))%R = Rsqr (vi intr).
proof: Proof. intro; rewrite <- Rsqr_mult; rewrite DRs; rewrite Rs_alphas; repeat rewrite Rsqr_mult; rewrite Rplus_comm; rewrite <- (Rmult_comm (Rsqr (cos (thetat t - alphas t)))); rewrite <- (Rmult_comm (Rsqr (sin (thetat t - alphas t)))); rewrite <- Rmult_plus_distr_r; rewrite sin2_cos2; rewrite Rmult_1_l; reflexivity. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho