proposition: Lemma Rsqr_u : forall (eps : posreal) (t : R), (0 <= t)%R -> (Rsqr (u0 t) <= Rsqr vi * Rsqr t + 2 * eps * vi * t)%R.
proof: Proof. intros; cut (u eps t <= vi * t + eps)%R. intro H0; generalize (u_pos eps t); intro H1; generalize (Rsqr_incr_1 (u eps t) (vi * t + eps) H0 H1 (Rle_trans 0 (u eps t) (vi * t + eps) H1 H0)); intro H2; rewrite Rsqr_plus in H2; rewrite Rsqr_u_epsilon in H2; rewrite Rsqr_mult in H2; rewrite <- (Rplus_comm (2 * (vi * t) * eps)) in H2; generalize (Rplus_le_compat_r (- Rsqr eps) (Rsqr (u0 t) + Rsqr eps) (2 * (vi * t) * eps + (Rsqr vi * Rsqr t + Rsqr eps)) H2); unfold Rminus in |- *; repeat rewrite Rplus_assoc; repeat rewrite Rplus_opp_r; repeat rewrite Rplus_0_r; intro H3; replace (Rsqr vi * Rsqr t + 2 * eps * vi * t)%R with (2 * (vi * t) * eps + Rsqr vi * Rsqr t)%R. assumption. ring. apply Rplus_le_reg_l with (- eps)%R; rewrite Rplus_comm; replace (- eps + (vi * t + eps))%R with (vi * t)%R. generalize (u_epsilon_le_vt eps t H); unfold Rminus in |- *; intro; assumption. ring. Qed.
imports: Reals trajectory_const rrho trajectory_def constants