proposition: Lemma r_sin_pos : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI)%R -> (0 <= r_vi * sin (rho_vi * t))%R.
proof: Proof. intros; apply Rmult_le_pos; [ left; unfold r_vi in |- *; unfold r in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ apply (TypeSpeed_pos (vi intr)) | apply Rinv_0_lt_compat; apply (rho_pos (vi intr)) ] | apply sin_ge_0; [ apply (rho_t_pos t H) | assumption ] ]. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega