proposition: Lemma D_F : forall t : R, derive_pt F t (F_derivable t) = (vi intr * cos (rho (vi intr) * (t / 2)))%R.
proof: Proof. intro; unfold F in |- *; reg. unfold Rdiv in |- *; field. assert (H0 := rho_pos (vi intr)); red in |- *; intro; rewrite H in H0; elim (Rlt_irrefl 0 H0). Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho