相关疑难解决方法(0)

我注意到在Coq对有理数的定义中,零的倒数被定义为零.(通常,除以零没有明确定义/合法/允许.)

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

为什么会这样？

它可能会导致有理数的计算出现问题,还是安全的？