proposition: Theorem YCNGFTYS : forall t : R, (0 <= t)%R -> (sqrt (Rsqr (xi t - xi 0) + Rsqr (yi t - yi 0)) <= v vi * t)%R.
proof: Proof. intros; apply Rsqr_incr_0. rewrite Rsqr_mult; apply le_epsilon; intros; generalize (Rsqr_u_Rsqr_vt (mkposreal eps H0) t H); simpl in |- *; unfold u0 in |- *; unfold xP, yP in |- *; intro H1; assumption. apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr. apply Rmult_le_pos; [ left; apply (TypeSpeed_pos vi) | assumption ]. Qed.
imports: Reals trajectory_const rrho trajectory_def constants