`BookProof.SqueezedGaussStates.Usum_identity` (v : ℝ) (M : ℕ) : (1 - 4 * v ^ 2) * Usum v M = Vsum v M - 4 * v ^ 2 * (2 * (M : ℝ) + 1) * Acoef v M

Initializing...

`BookProof.SqueezedGaussStates.Usum_identity` (v : ℝ) (M : ℕ) : (1 - 4 * v ^ 2) * Usum v M = Vsum v M - 4 * v ^ 2 * (2 * (M : ℝ) + 1) * Acoef v M · Prove2Me