Describir: Verificación formal y programación certificada en COQ con Program : un ejemplo práctico