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