%======================================================================
\section{Conclusion}\label{s:conclusion}

We draw two lessons that may carry over to formalizations of other long analytic proofs. First, arguments that a paper
borrows ``with changes'' are best written out in full, inputs and outputs included, before anyone formalizes them. Second,
when the parts of a proof are joined by interfaces, each interface needs its own check that the objects the proof
actually produces satisfy it (\S\ref{ss:guards}).