Noté que en la definición de racional de Coq, el inverso de cero se define a cero. (Por lo general, la división por cero no está bien definida / legal / permitida).

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

¿Por que es esto entonces?

¿Podría causar problemas en los cálculos con racionales, o es seguro?