Notei que, na definição de racional de Coq, o inverso de zero é definido como zero. (Normalmente, a divisão por zero não é bem definida / legal / permitida.)

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

Por que é tão?

Poderia causar problemas nos cálculos com argumentos racionais ou é seguro?