simp
case h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 6 → M
nₖ : M
a✝ : nₖ ≤ v 5
⊢ Series (v 0) (v 1) (v 2) (v 3) (v 4 / ‖v 1‖) nₖ ∧
      Segment (v 0) (v 2) (v 3) (‖v 1‖ * (v 4 / ‖v 1‖)) (v 4 % ‖v 1‖) nₖ (v 5) ↔
    ‖v 1‖ ≤ v 1 ∧
      v 4 / ‖v 1‖ ≤ v 4 ∧
        v 4 % ‖v 1‖ ≤ v 4 ∧
          Series (v 0) (v 1) (v 2) (v (Fin.succ 2)) (v 4 / ‖v 1‖) nₖ ∧
            Segment (v 0) (v 2) (v (Fin.succ 2)) (‖v 1‖ * (v 4 / ‖v 1‖)) (v 4 % ‖v 1‖) nₖ (v 5)
case h.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
v : Fin 6 → M
nₖ : M
a✝ : nₖ ≤ v 5
⊢ Series (v 0) (v 1) (v 2) (v 3) (v 4 / ‖v 1‖) nₖ ∧
      Segment (v 0) (v 2) (v 3) (‖v 1‖ * (v 4 / ‖v 1‖)) (v 4 % ‖v 1‖) nₖ (v 5) ↔
    Series (v 0) (v 1) (v 2) (v (Fin.succ 2)) (v 4 / ‖v 1‖) nₖ ∧
      Segment (v 0) (v 2) (v (Fin.succ 2)) (‖v 1‖ * (v 4 / ‖v 1‖)) (v 4 % ‖v 1‖) nₖ (v 5)