proposition: Lemma u_epsilon_le_vt : forall (eps : posreal) (t : R), (0 <= t)%R -> (u eps t - eps <= vi * t)%R.
proof: Proof. intros. generalize (IAF_var (fun t : R => (vi * t)%R) (fun t : R => u eps t) 0 t vit_derivable (d_u eps) H); intros. cut (u eps 0 = eps). intro H1. rewrite <- H1. elim H0; intros. rewrite Rmult_0_r in H2; unfold Rminus in H2; rewrite Ropp_0 in H2; rewrite Rplus_0_r in H2; left; assumption. rewrite Rmult_0_r in H2; unfold Rminus in H2; rewrite Ropp_0 in H2; rewrite Rplus_0_r in H2; right; assumption. rewrite (derive_vit c); apply (u_epsilon_le_v eps c). unfold u in |- *; unfold xP in |- *; unfold yP in |- *; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; rewrite Rsqr_0; repeat rewrite Rplus_0_l; apply (sqrt_Rsqr eps (Rlt_le 0 eps (cond_pos eps))). Qed.
imports: Reals trajectory_const rrho trajectory_def constants