Theorem: VehicleSpeedSched.nₚ_pos (CvxLean/Examples/VehicleSpeedScheduling.lean)

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

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