Proving Bounds for the Randomized MaxCut Approximation Algorithm in Lean4