SBS Lean proofs

Lean formalization of the proof on the upper bound of the probability for LIPO to reject a candidate. The Lean files are available on GitHub.