何度目か分からないが、 $\mathbb{X}$ で、小学の算数テストで0で割った答えがどうこうのという話題を見て、思い出したので書いておく。
言うまでもないが、Coqと小学生の算数テストの間には特に関係がない。

Vanilla Coqでのnatの除算

divの定義を見ると、 0 で割ると 0 になることは定義から分かる。 (y が 0 のとき、 y を返すのだからそう)

divの定義

Definition div x y :=
  match y with
    | 0 => y
    | S y' => fst (divmod x y' 0 y')
  end.

そうすると、気になるのが、矛盾とかが出てきて困らないの?ということだが、特に矛盾は出てきていないっぽい。

x / y = z のとき x = y * z になるはずだけど、 y = 0 だとそれが成り立たない、という話は真っ先に思いつくはずだ。それはその通りである。

x / y = zならばx = y * zが一般には成り立たないことの証明

Goal ~(forall x y z, (Nat.div x y) = z -> x = y * z).
intro H.
assert (1 = 0 * 0) as C.
  apply H; easy.
discriminate C.
Qed.

しかし、Coqの div は割り算の余りは無視する定義になっているので、y = 0 でなくても x / y = z -> x = y * z は成り立たない。

yが0ではない場合にx / y = zならばx = y * zが一般には成り立たないことの証明

Goal ~(forall x y z, y <> 0 /\ (Nat.div x y) = z -> x = y * z).
intro H.
assert (3 = 2 * 1) as C.
  apply H; easy.
discriminate C.
Qed.

なお、 y = 0 以外での除算に関しては、除算と剰余のペアを返す関数 divmod を通じて定義されている。少し変更すれば、ここでの場合分けは不要となるはずである(もちろん、 divmod では場合分けは発生する。次に見るMathComp/ssreflectでは現にそのように定義されている)。

MathComp/ssreflectでのssrnatの除算

ssrnatでは、除算(divn)は、

divnの定義

Definition edivn_rec d :=
  fix loop m q := if m - d is m'.+1 then loop m' q.+1 else (q, m).

Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).

Definition divn m d := (edivn m d).1.

と定義されている。記法が独特で慣れないが、除算と剰余のペアを返す関数 edivn の1つ目の要素を返す形で divn が定義されている。

edivn の定義より、 edivn x 0 は (0, x) となることが分かるので、 divn x 0 = 0 となる。
これは divn0 という名前のLemmaが示されている。

ssrnatには、これらを利用したLemmaがたくさん示されている。これらは、0除算を避けられているものもあれば、0より大きいことを明示的に条件に入れているものもある。

例えば、除算結果の不等号に関する補題を2つ見る。

除算結果の不等号に関する補題 `leq_div2r`

leq_div2r は、 $m \le n$ ならば $m / d \le m / n$ が成り立つ、という補題である。

leq_div2r

Lemma leq_div2r d m n : m <= n -> m %/ d <= n %/ d.

$d = 0$ のとき、今回の定義では、 $m / d$ も $n / d$ も共に 0 になるので、この補題は $d = 0$ においても成り立つ。

除算結果の不等号に関する補題 `leq_div2l`

leq_div2l は、 $0 < d$ かつ $d \le e$ ならば、 $m / e \le m / d$ が成り立つという補題である。

leq_div2l

Lemma leq_div2l m d e : 0 < d -> d <= e -> m %/ e <= m %/ d.

これは、 $d = 0$ は条件により明示的に避けられている。もしこの条件がなければ、$d = 0, m / e > 0$ のときに補題が成り立たない(たとえば$m = 1, d = 0, e = 1$のとき)。