proposition: Lemma MinDistance_lb_0 : (MinDistance_lb <= MinDistance)%R.
proof: Proof. Proof with trivial. unfold MinDistance_lb, MinDistance in |- *; unfold Rminus in |- *; rewrite (Rplus_comm (m_rho_ub MinT)); rewrite (Rplus_comm (m T)); apply Rplus_le_compat_l... cut (MinT <= MinT)%R... intro H; apply Rle_trans with (m MinT)... apply (m_rho_ub_0 (mkTimeT MinT H MinT_MaxT))... apply (m_le (mkTimeT MinT H MinT_MaxT) T)... simpl in |- *; apply (cond_1 T)... right... Qed.
imports: Reals trajectory_const rrho trajectory_def