\section{Proving that X25519 in Coq matches the mathematical model}