adapt to Isabelle d3d91422f408 (moments of normal distribution)
moved Real_to_Complex into Isabelle repo; moved auxiliary lemmas to Library_Misc
first round moving to Isabelle