\section{Proof}

\subsection{Coq Mechanisation}