Short answer: yes, it is absolutely safe.
When we say that division by zero is not defined, we actually mean that zero has no multiplicative inverse. In particular, we cannot have a function that computes the multiplicative inverse of zero. However, you can write a function that calculates the multiplicative inverse for all other elements and returns some arbitrary value if such an inverse does not exist (for example, for zero). This is exactly what this function does.
The definition of this inverse operator everywhere means that we can define other functions that are evaluated with it, without having to explicitly state that its argument is nonzero, which makes it more convenient to use. In fact, imagine what a pain it would be if we made this function a returned option instead, without getting a null value: we would have to make all our code monadic, which makes understanding and reasoning difficult. We would have a similar problem when writing a function that requires proof that its argument is nonzero.
So what is the catch? Well, when we try to prove something about a function using the inverse operator, we will need to add explicit hypotheses saying that we pass it an argument other than zero, or assert that its argument can never be zero. Lemmas about this function then receive additional premises, for example
forall q, q <> 0 -> q * (/ q) = 1
Many other libraries are structured this way, cf. for example, the definition of field axioms in the MathComp algebra library.
There are some cases when we want to learn the additional prerequisites required by some functions, such as type restrictions. This is what we do, for example, when we use vectors with a length index and the safe get function, which can only be called for numbers within the bounds. So, how do we decide which one should be used when developing the library, that is, use a rich type with a lot of additional information and prevent fictitious calls to certain functions (as in the case of the length index) or leave this information and require it as explicit lemmas ( as in the multiplicative converse case)? Well, there is no definite answer, and you need to really analyze each case individually and decide which alternative will be better for this particular case.