The original proof I posted was organized slightly differently from your argument. Some of those 120 lines were commentary, blanks and things like "qed". Also,

The original proof I posted was organized slightly differently from your argument. Some of those 120 lines were commentary, blanks and things like "qed". Also, I tried to used small steps in the proof. You can have a more concise proof if you are willing to take larger steps and rely more on automation. The cost is that the justification for the steps might become opaque to humans. Here is a second attempt at the proof that follows your argument and uses more automation. It is much shorter than the original: https://gist.github.com/jmoy/27bcc72fb5a3f871b72c31e81bccb55f https://gist.github.com/jmoy/27bcc72fb5a3f871b72c31e81bccb55...