Thanks for the feedback - I figured presenting the exact Coq proofs directly would probably be too dry, and thus was trying to give some context for the work to

Thanks for the feedback - I figured presenting the exact Coq proofs directly would probably be too dry, and thus was trying to give some context for the work to make the presentation more interesting. In hindsight, I can see how this has been detrimental to some other parts of the article. If you look at the related work section of the paper, we actually present a multitude of papers in the literature (even some recent as 2019) that actually still incorrectly refer to Bloom's expression as an exact bound, so I thought at the time that the "debunking" title was not inaccurate. I'll keep your advice in mind the next time I write an article about research work.