Ok but how often do people provide a proof assistant verified proof for it? That's what this is. (Except that it's because the verifier had a bug.)