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

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

State before:
n : ℕ
d τmin τmax smin smax : Fin n → ℝ
F : ℝ → ℝ
i : Fin nₚ
⊢ 0 i < sminₚ i
Tactic:
fin_cases i <;> norm_num
State after:
no goals