`BookProof.FockQuadratic.wsum_tsub_of_le` {ω : ι → ℝ} {P a : Idx ι} (h : P ≤ a) : wsum ω (a

Initializing...

`BookProof.FockQuadratic.wsum_tsub_of_le` {ω : ι → ℝ} {P a : Idx ι} (h : P ≤ a) : wsum ω (a - P) + wsum ω P = wsum ω a · Prove2Me