proposition: Lemma xp_pos : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI)%R -> Omega (beta + thetat intr 0) = true -> (0 <= xp t)%R.
proof: Proof. intros; apply Rle_trans with (r_vi * sin (rho_vi * t))%R; [ apply Rmult_le_pos; [ unfold r_vi in |- *; unfold r in |- *; left; unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ apply TypeSpeed_pos | apply Rinv_0_lt_compat; apply rho_pos ] | apply sin_ge_0; [ apply Rmult_le_pos; [ unfold rho_vi in |- *; left; apply rho_pos | assumption ] | assumption ] ] | apply (xpt_Omega t H H0 H1) ]. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega