Derivative continuity for the homotopy on partition pieces

Proves that the t-derivative of fdBoundaryToPolygonHomotopy is continuous on each partition piece (p₁, p₂) × [0, 1], where (p₁, p₂) avoids the partition points {1, 2, 3, 4}.

theorem RectHomotopyProof.fdBoundaryToPolygonHomotopy_deriv_continuousOn_pieces (p₁ p₂ : ℝ) (hp₁p₂ : p₁ < p₂) (hpiece : ∀ t ∈ Set.Ioo p₁ p₂, t ∉ {1, 2, 3, 4}) (h_sub : Set.Ioo p₁ p₂ ⊆ Set.Ioo 0 5) : ContinuousOn (fun (q : ℝ × ℝ) => deriv (fun (t' : ℝ) => fdBoundaryToPolygonHomotopy (t', q.2)) q.1) (Set.Ioo p₁ p₂ ×ˢ Set.Icc 0 1)