The Lean 4 theorem `symmetricOn_add` in the `ChapterKatoRellichRelative` chapter of the timepiece formalization

-- Generated from ChapterKatoRellichRelative.lean — theorem BookProof.KatoRellich.symmetricOn_add
import Mathlib
import Definitions.Def_ChapterKatoRellichRelative
import Definitions.Def_ChapterEsaClosureCore



open BookProof.FarisLavine

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] {D : Submodule ℂ F}

theorem BookProof.KatoRellich.symmetricOn_add {H B : D →ₗ[ℂ] F} (hH : SymmetricOn D H) (hB : SymmetricOn D B) :
    SymmetricOn D (H + B) := by sorry