Comment by jboggan

Ah, cool. I'm still learning Lean - is there somewhere else in the repo with the Lean specification of the cycle construction for the full argument?