proposition: Lemma D_F_Rsqr_v : forall t : R, (Rsqr (derive_pt F t (F_derivable t)) + Rsqr (rho (vi intr) / 2) * Rsqr (F t))%R = Rsqr (vi intr).
proof: Proof. intro; rewrite (D_F t); rewrite <- Rsqr_mult; cut ((rho (vi intr) / 2 * F t)%R = (vi intr * sin (rho (vi intr) * (t / 2)))%R). intro H; rewrite H; repeat rewrite Rsqr_mult; replace (Rsqr (vi intr) * Rsqr (cos (rho (vi intr) * (t / 2))) + Rsqr (vi intr) * Rsqr (sin (rho (vi intr) * (t / 2))))%R with (Rsqr (vi intr) * (Rsqr (sin (rho (vi intr) * (t / 2))) + Rsqr (cos (rho (vi intr) * (t / 2)))))%R. rewrite sin2_cos2; rewrite Rmult_1_r; reflexivity. ring. unfold F in |- *; unfold Rdiv in |- *; rewrite <- Rmult_assoc; replace (rho (vi intr) * / 2 * (2 * (vi intr * / rho (vi intr))))%R with (2 * / 2 * (rho (vi intr) * / rho (vi intr)) * vi intr)%R. repeat rewrite <- Rinv_r_sym. repeat rewrite Rmult_1_l; reflexivity. generalize (rho_pos (vi intr)); intro; red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl 0 H). discrR. ring. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho