Demonstration, in Coq, that the Euclidean Algorithm can be efficiently used to compute the greatest common divisor of two numbers a and b in O(log(min(a, b))) steps.
This project was implemented as part of my undergradute scientific initiation program in formal software verification, supervised by Flávio L. C. Moura, in 2009.