Theorem: VehicleSpeedSched.aₚ_nonneg (CvxLean/Examples/VehicleSpeedScheduling.lean)

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ aₚ
Tactic:
unfold aₚ
State after:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ 1

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals