proposition: Lemma Rsqr_u_Rsqr_vt : forall (eps : posreal) (t : R), (0 <= t)%R -> (Rsqr (u0 t) <= Rsqr vi * Rsqr t + eps)%R.
proof: Proof. intros; case (Rtotal_order 0 t); intro. cut (0 < eps / (2 * vi * t))%R. intro; generalize (Rsqr_u (mkposreal (eps / (2 * vi * t)) H1) t H); simpl in |- *; replace (2 * (eps / (2 * vi * t)) * vi * t)%R with (eps * 1)%R. rewrite Rmult_1_r; intro; assumption. unfold Rdiv in |- *; repeat rewrite Rinv_mult_distr. replace (2 * (eps * (/ 2 * / vi * / t)) * vi * t)%R with (eps * (2 * / 2) * (/ vi * vi) * (/ t * t))%R. repeat rewrite <- Rinv_l_sym. rewrite <- Rinv_r_sym. repeat rewrite Rmult_1_r; reflexivity. discrR. red in |- *; intro H2; rewrite H2 in H0; elim (Rlt_irrefl 0 H0). generalize (TypeSpeed_pos vi); intro H2; red in |- *; intro H3; rewrite H3 in H2; elim (Rlt_irrefl 0 H2). ring. discrR. generalize (TypeSpeed_pos vi); intro H2; red in |- *; intro H3; rewrite H3 in H2; elim (Rlt_irrefl 0 H2). apply prod_neq_R0. discrR. generalize (TypeSpeed_pos vi); intro H2; red in |- *; intro H3; rewrite H3 in H2; elim (Rlt_irrefl 0 H2). red in |- *; intro H2; rewrite H2 in H0; elim (Rlt_irrefl 0 H0). unfold Rdiv in |- *; apply Rmult_lt_0_compat. apply (cond_pos eps). apply Rinv_0_lt_compat; repeat apply Rmult_lt_0_compat. prove_sup0. apply (TypeSpeed_pos vi). assumption. elim H0; intro. rewrite <- H1; unfold u0 in |- *; unfold xP, yP in |- *; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; repeat rewrite Rsqr_0; rewrite Rmult_0_r; repeat rewrite Rplus_0_l; rewrite sqrt_0; rewrite Rsqr_0; left; apply (cond_pos eps). elim (Rlt_irrefl 0 (Rle_lt_trans 0 t 0 H H1)). Qed.
imports: Reals trajectory_const rrho trajectory_def constants