proposition: Lemma xpt_pos : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI)%R -> (0 <= xp t - xp 0)%R.
proof: Proof. intros; generalize (xpt t H H0); unfold hx in |- *; intro; apply Rle_trans with (r_vi * sin (rho_vi * t))%R; [ apply (r_sin_pos t H H0) | assumption ]. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega