proposition: Lemma u_epsilon_le_v : forall (eps : posreal) (t : R), (derive_pt (u eps) t (d_u eps t) <= vi)%R.
proof: Proof. intros. generalize (D_Rsqr_u_epsilon_2 eps t); intro H. rewrite (D_Rsqr_u_epsilon_1 eps t) in H. repeat rewrite Rmult_assoc in H. assert (Hyp : (0 < 2)%R). prove_sup0. generalize (Rmult_le_reg_l 2 (u eps t * derive_pt (u eps) t (d_u eps t)) (u0 t * vi) Hyp H); intro H1. generalize (u0_u_epsilon eps t); intro H2; generalize (Rmult_le_compat_r (v vi) (u0 t) (u eps t) (Rlt_le 0 vi (TypeSpeed_pos vi)) H2); intro H3. generalize (Rle_trans (u eps t * derive_pt (u eps) t (d_u eps t)) (u0 t * vi) (u eps t * vi) H1 H3); intro H4. apply (Rmult_le_reg_l (u eps t) (derive_pt (u eps) t (d_u eps t)) vi (u_stric_pos eps t) H4). Qed.
imports: Reals trajectory_const rrho trajectory_def constants