proposition: Lemma xpt : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI)%R -> (hx t <= xp t - xp 0)%R.
proof: Proof. intros; replace (hx t) with (hx t - hx 0)%R. apply (IAF_var xp hx 0 t xp_derivable hx_derivable H); intros; rewrite Dhx; elim H1; intros; apply (Dx0_PI c H2 (Rle_trans (rho_vi * c) (rho_vi * t) PI (rho_t_le c t H3) H0)). unfold hx in |- *; rewrite Rmult_0_r; rewrite sin_0; unfold Rminus in |- *; rewrite Rmult_0_r; rewrite Ropp_0; apply Rplus_0_r. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega