Imp: Adds proof for optimize_0plus_b