proposition: Lemma MaxDistance_ub_0 : (MaxDistance <= MaxDistance_ub)%R.
proof: Proof. unfold MaxDistance, MaxDistance_ub in |- *. rewrite (Rplus_comm (V * T)). rewrite (Rplus_comm (V * MaxT)). apply Rplus_le_compat_l. apply Rmult_le_compat_l. left; apply (TypeSpeed_pos V). apply (cond_2 T). Qed.
imports: Reals trajectory_const rrho trajectory_def