proposition: Lemma u0_pos : forall t : R, (0 <= u0 t)%R.
proof: Proof. intros; unfold u0 in |- *; apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr. Qed.
imports: Reals trajectory_const rrho trajectory_def constants