[math-fun] Mysterious but well-known identity