The finite next-bit prediction experiment -- proof internals

theorem Complexity.NextBitPrediction.successProbability_eq_half_add_gap_internal {background : Type u_1} [Fintype background] [Nonempty background] (target : background → Bool) (testAt : background → Bool → Bool) : successProbability target testAt = 1 / 2 + targetAcceptanceProbability target testAt - candidateAcceptanceProbability testAt