Infinitary Rewriting in Coq