proposition: Lemma u0_u_epsilon : forall (eps : posreal) (t : R), (u0 t <= u eps t)%R.
proof: Proof. intros; apply Rsqr_incr_0; [ unfold u0, u in |- *; repeat rewrite Rsqr_sqrt; [ rewrite <- (Rplus_0_r (Rsqr (xP t) + Rsqr (yP t))); repeat rewrite Rplus_assoc; repeat apply Rplus_le_compat_l; rewrite Rplus_0_l; apply Rle_0_sqr | repeat apply Rplus_le_le_0_compat; apply Rle_0_sqr | apply Rplus_le_le_0_compat; apply Rle_0_sqr ] | apply u0_pos | apply u_pos ]. Qed.
imports: Reals trajectory_const rrho trajectory_def constants