proposition: Lemma xpt_Omega : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI)%R -> Omega (beta + thetat intr 0) = true -> (r_vi * sin (rho_vi * t) <= xp t)%R.
proof: Proof. intros; generalize (xpt t H H0); intro; generalize (xp0_pos H1); intro; unfold hx in H2; generalize (Rplus_le_compat_r (xp 0) (r_vi * sin (rho_vi * t)) (xp t - xp 0) H2); unfold Rminus in |- *; repeat rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; intro; apply (plus_le_is_le (r_vi * sin (rho_vi * t)) (xp 0) (xp t) H3 H4). Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega