In this paper we present Coq-HOL-Light, a library with more than 20,000 mathematical theorems on real analysis in Rocq. This library is a translation from the HOL-Light proof assistant. By proving the equivalence between a number of types, functions and predicates in HOL-Light and their counterpart in the Rocq standart library, we make this library directly usable in Rocq developments. We also present our indexing and retrieval tools, specially tailored for searching mathematical entities in the Coq-HOL-Light library with special facilities for the Rocq community. All tools underpinning out methodology are publicly available guarantying the reproducibility of the processes detailed in this paper. We argue that this work is relevant to researchers and practitioners who wish to harness HOL-Light’s comprehensive analysis library to support the construction of Rocq developments.