Verification of the algorithm described in "On building trees of minimal height" by Richard S. Bird, using Coq