Coq QArith Division durch Null ist Null, warum?

Ich habe festgestellt, dass in Coqs Definition von Rationalen die Umkehrung von Null zu Null definiert ist. (Normalerweise ist die Division durch Null nicht genau definiert / zulässig / zulässig.)

Require Import QArith.
Lemma inv_zero_is_zero: (/ 0) == 0. 
Proof. unfold Qeq. reflexivity. Qed.

Wieso ist es so

Könnte es Probleme bei der Berechnung von Rationalen geben, oder ist es ungefährlich?