You'd be surprised how simple a well written proof can be compared to a program implementing an algorithm to do the same.

That said, Coq itself is not the best vehicle for this. There are nicer high order logic languages.