CH2.conj_intHSeg_of_antisymm

lemma conj_intHSeg_of_antisymm (h a b : ℝ) (F : ℂ → ℂ) (hF : ∀ s, starRingEnd ℂ (F s) = -F (starRingEnd ℂ s)) :    starRingEnd ℂ (intHSeg h a b F) = intHSeg (-h) b a F := by  unfold intHSeg  rw [← intervalIntegral_conj]  have h_integrand : ∀ t : ℝ, starRingEnd ℂ (F (↑t + ↑h * I)) = - F (↑t + ↑(-h) * I) := by    intro t    have h1 : starRingEnd ℂ (↑t + ↑h * I) = ↑t + ↑(-h) * I := by      rw [map_add, map_mul, conj_ofReal, conj_ofReal, conj_I]      push_cast      ring    have h2 := hF (↑t + ↑h * I)    rw [h1] at h2    rw [h2]  simp_rw [h_integrand]  rw [intervalIntegral.integral_symm, intervalIntegral.integral_neg, neg_neg]