First proof of zeta(2)

Stream: Proofs from the book

[Julien Michel]

Hi, over the last few days I've formalized here the first proof of ζ(2) = π^2 / 6 from chapter 9 (the one computing ∫ x : ℝ in 0..1, ∫ y : ℝ in 0..1, 1 / (1 - x*y)in two different ways). Here is my PR #105.
I also submitted a bump PR #104.
Any comments welcome!