proposition: Lemma rho_t_le : forall t1 t2 : R, (t1 <= t2)%R -> (rho_vi * t1 <= rho_vi * t2)%R.
proof: Proof. Proof with trivial. intros; apply Rmult_le_compat_l... left; unfold rho_vi in |- *; apply rho_pos... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega