remove redundant lemma real_sum_squared_expand in favor of power2_sum
By chapter:chapters 1 and 2, maybe 3: Peter Whitechapters 6, 7 and 8: David von Oheimchapter 6, maybe 8: Gerwin Kleinchapters 3, maybe 4: Tanja Voschapters 1-3 at least: Stefano Bistarelli