[xgk]

   Can this be done with Coq?

This can be done with any prover.

Simplifying a bit, an algorithm is a function of type A -> B. If you have two implementations, f1 :: A -> B and f2 :: A -> B, say one slow and simple (f1), one fast and complicated (f2), then you can verify that f2 does what it is supposed to do in two steps:

1. Show that for all a in A we have f1 a == f2 a.

2. Show that f1 meets the specification.

If you trust that f1 does what it is supposed to do, then you can skip (2).